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

A1: ( T is bijective & T = MorphsZQ L & ( for v being Vector of L holds T . v = Class ((EQRZM L),[v,1]) ) ) by ZMODUL08:21;

set v = the non zero Vector of L;

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

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

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

then T . the non zero Vector of L <> 0. (EMLat L) by defEMLat;

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

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

hence not EMLat L is trivial by ZMODUL07:41; :: thesis: verum

A1: ( T is bijective & T = MorphsZQ L & ( for v being Vector of L holds T . v = Class ((EQRZM L),[v,1]) ) ) by ZMODUL08:21;

set v = the non zero Vector of L;

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

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

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

proof

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

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

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

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

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

then T . the non zero Vector of L <> 0. (EMLat L) by defEMLat;

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

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

hence not EMLat L is trivial by ZMODUL07:41; :: thesis: verum