consider T being linear-transformation of (EMbedding V),(EMbedding (r,V)) such that
A1: ( ( for v being Element of (Z_MQ_VectSp V) st v in EMbedding V holds
T . v = r * v ) & T is bijective ) by rSB03A;
set v = the non zero Vector of (EMbedding V);
T . the non zero Vector of (EMbedding V) <> 0. (EMbedding (r,V))

proof

assume T . the non zero Vector of (EMbedding V) = 0. (EMbedding (r,V)) ; :: thesis: contradiction
then T . the non zero Vector of (EMbedding V) = T . (0. (EMbedding V)) by ZMODUL05:19;
hence contradiction by A1, FUNCT_2:19; :: thesis: verum

end;

then not T . the non zero Vector of (EMbedding V) in (0). (EMbedding (r,V)) by ZMODUL02:66;
then (Omega). (EMbedding (r,V)) <> (0). (EMbedding (r,V)) ;
hence not EMbedding (r,V) is trivial by ZMODUL07:41; :: thesis: verum