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)

proof

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 <> zeroCoset L by ZMODUL08:def 3;
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