consider T being linear-transformation of V,(EMbedding V) such that
A1: ( T is bijective & T = MorphsZQ V & ( for v being Vector of V holds T . v = Class ((EQRZM V),[v,1]) ) ) by SB03;
set v = the non zero Vector of V;
T . the non zero Vector of V <> 0. (EMbedding V)
proof
assume T . the non zero Vector of V = 0. (EMbedding V) ; :: thesis: contradiction
then T . the non zero Vector of V = T . (0. V) by ZMODUL05:19;
hence contradiction by A1, FUNCT_2:19; :: thesis: verum
end;
then not T . the non zero Vector of V in (0). (EMbedding V) by ZMODUL02:66;
then (Omega). (EMbedding V) <> (0). (EMbedding V) ;
hence not EMbedding V is trivial by ZMODUL07:41; :: thesis: verum