per cases ( r is zero or not r is zero ) ;

suppose B1: r is zero ; :: thesis: EMbedding (r,V) is finitely-generated

B2: for v being Vector of (Z_MQ_VectSp V) st v in r * (rng (MorphsZQ V)) holds
v = 0. (Z_MQ_VectSp V)

proof

let v be Vector of (Z_MQ_VectSp V); :: thesis: ( v in r * (rng (MorphsZQ V)) implies v = 0. (Z_MQ_VectSp V) )
assume C1: v in r * (rng (MorphsZQ V)) ; :: thesis: v = 0. (Z_MQ_VectSp V)
consider u being Vector of (Z_MQ_VectSp V) such that
C2: ( v = (0. F_Rat) * u & u in rng (MorphsZQ V) ) by B1, C1;
thus v = 0. (Z_MQ_VectSp V) by C2, VECTSP_1:14; :: thesis: verum

end;

B3: EMbedding (r,V) is strict Submodule of DivisibleMod V by ThDivisible3;
for v being Vector of (DivisibleMod V) holds
( v in EMbedding (r,V) iff v in (0). (DivisibleMod V) )

proof

let v be Vector of (DivisibleMod V); :: thesis: ( v in EMbedding (r,V) iff v in (0). (DivisibleMod V) )

hereby :: thesis: ( v in (0). (DivisibleMod V) implies v in EMbedding (r,V) )

assume v in EMbedding (r,V) ; :: thesis: v in (0). (DivisibleMod V)
then v in r * (rng (MorphsZQ V)) by defriV;
then v = 0. (Z_MQ_VectSp V) by B2
.= 0. (DivisibleMod V) by ThDivisibleX1 ;
hence v in (0). (DivisibleMod V) by ZMODUL02:66; :: thesis: verum

end;

assume v in (0). (DivisibleMod V) ; :: thesis: v in EMbedding (r,V)
then v = 0. (DivisibleMod V) by ZMODUL02:66
.= 0. (EMbedding (r,V)) by B3, ZMODUL01:26 ;
hence v in EMbedding (r,V) ; :: thesis: verum

end;

hence EMbedding (r,V) is finitely-generated by B3, ZMODUL01:46; :: thesis: verum

end;

suppose not r is zero ; :: thesis: EMbedding (r,V) is finitely-generated

then consider T being linear-transformation of (EMbedding V),(EMbedding (r,V)) such that
A1: ( ( for v being Vector of (Z_MQ_VectSp V) st v in EMbedding V holds
T . v = r * v ) & T is bijective ) by rSB03A;
reconsider Z = EMbedding (r,V) as free Z_Module by A1, ZMODUL06:48;
Z is finite-rank by A1, ZMODUL06:50;
hence EMbedding (r,V) is finitely-generated ; :: thesis: verum

end;

end;