consider A being finite Subset of V such that
A1: Lin A = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) by ZMODUL03:def 4;
set T = ZQMorph (V,W);
reconsider B = (ZQMorph (V,W)) .: A as finite Subset of (VectQuot (V,W)) ;
A2: (ZQMorph (V,W)) .: the carrier of (Lin A) c= the carrier of (Lin B) by ZMODUL06:40;
A3: rng (ZQMorph (V,W)) = the carrier of (VectQuot (V,W)) by FUNCT_2:def 3;
X1: rng (ZQMorph (V,W)) = (ZQMorph (V,W)) .: (dom (ZQMorph (V,W))) by RELAT_1:113
.= (ZQMorph (V,W)) .: the carrier of (Lin A) by A1, FUNCT_2:def 1 ;
the carrier of (Lin B) c= the carrier of (VectQuot (V,W)) by VECTSP_4:def 2;
hence VectQuot (V,W) is finitely-generated by A2, A3, X1, XBOOLE_0:def 10, ZMODUL01:47; :: thesis: verum