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))
proof
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) <> zeroCoset L by ZMODUL08:def 6;
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