proposition: Lemma aimgM (f : ahom aT rT) U V : (f @: (U * V) = f @: U * f @: V)%VS.
proof: Proof. apply/eqP; rewrite eqEsubv; apply/andP; split; last first. apply/prodvP=> _ _ /memv_imgP[u Hu ->] /memv_imgP[v Hv ->]. by rewrite -rmorphM memv_img // memv_mul. apply/subvP=> _ /memv_imgP[w UVw ->]; rewrite memv_preim (subvP _ w UVw) //. by apply/prodvP=> u v Uu Vv; rewrite -memv_preim rmorphM memv_mul // memv_img. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype div tuple finfun bigop ssralg) mathcomp(finalg zmodp matrix vector poly)