consider T being linear-transformation of (EMbedding L),(EMbedding (r,L)) such that

A1: ( ( for v being Element of (Z_MQ_VectSp L) st v in EMbedding L holds

T . v = r * v ) & T is bijective ) by ZMODUL08:27;

set v = the non zero Vector of (EMbedding L);

T . the non zero Vector of (EMbedding L) in the carrier of (EMbedding (r,L)) ;

then A2: T . the non zero Vector of (EMbedding L) in r * (rng (MorphsZQ L)) by ZMODUL08:def 6;

T . the non zero Vector of (EMbedding L) <> 0. (EMbedding (r,L))

then T . the non zero Vector of (EMbedding L) <> 0. (EMLat (r,L)) by defrEMLat;

then not T . the non zero Vector of (EMbedding L) in (0). (EMLat (r,L)) by ZMODUL02:66;

then (Omega). (EMLat (r,L)) <> (0). (EMLat (r,L)) by A2, defrEMLat;

hence not EMLat (r,L) is trivial by ZMODUL07:41; :: thesis: verum

A1: ( ( for v being Element of (Z_MQ_VectSp L) st v in EMbedding L holds

T . v = r * v ) & T is bijective ) by ZMODUL08:27;

set v = the non zero Vector of (EMbedding L);

T . the non zero Vector of (EMbedding L) in the carrier of (EMbedding (r,L)) ;

then A2: T . the non zero Vector of (EMbedding L) in r * (rng (MorphsZQ L)) by ZMODUL08:def 6;

T . the non zero Vector of (EMbedding L) <> 0. (EMbedding (r,L))

proof

then
T . the non zero Vector of (EMbedding L) <> zeroCoset L
by ZMODUL08:def 6;
assume
T . the non zero Vector of (EMbedding L) = 0. (EMbedding (r,L))
; :: thesis: contradiction

then T . the non zero Vector of (EMbedding L) = T . (0. (EMbedding L)) by ZMODUL05:19;

hence contradiction by A1, FUNCT_2:19; :: thesis: verum

end;then T . the non zero Vector of (EMbedding L) = T . (0. (EMbedding L)) by ZMODUL05:19;

hence contradiction by A1, FUNCT_2:19; :: thesis: verum

then T . the non zero Vector of (EMbedding L) <> 0. (EMLat (r,L)) by defrEMLat;

then not T . the non zero Vector of (EMbedding L) in (0). (EMLat (r,L)) by ZMODUL02:66;

then (Omega). (EMLat (r,L)) <> (0). (EMLat (r,L)) by A2, defrEMLat;

hence not EMLat (r,L) is trivial by ZMODUL07:41; :: thesis: verum