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; verum