suppose B1: r is zero ; :: thesis:

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

let v be Vector of (Z_MQ_VectSp V); :: thesis:
assume C1: v in r * (rng (MorphsZQ V)) ; :: thesis:
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:

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) )

let v be Vector of (DivisibleMod V); :: thesis:

hereby :: thesis:

assume v in EMbedding (r,V) ; :: thesis:
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:

end;

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

end;

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

end;

suppose not r is zero ; :: thesis:

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:

end;

end;