let L be Z_Lattice; :: thesis: for x being object holds
( x is Vector of (EMLat L) iff x is Vector of (EMbedding L) )
let x be object ; :: thesis: ( x is Vector of (EMLat L) iff x is Vector of (EMbedding L) )
hereby :: thesis: ( x is Vector of (EMbedding L) implies x is Vector of (EMLat L) )
assume x is Vector of (EMLat L) ; :: thesis: x is Vector of (EMbedding L)
then x in ModuleStr(# the carrier of (EMLat L), the addF of (EMLat L), the ZeroF of (EMLat L), the lmult of (EMLat L) #) ;
hence x is Vector of (EMbedding L) by LmEMDetX0; :: thesis: verum
end;
assume x is Vector of (EMbedding L) ; :: thesis: x is Vector of (EMLat L)
then x in EMbedding L ;
then x in ModuleStr(# the carrier of (EMLat L), the addF of (EMLat L), the ZeroF of (EMLat L), the lmult of (EMLat L) #) by LmEMDetX0;
hence x is Vector of (EMLat L) ; :: thesis: verum