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) )

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

( 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 (EMbedding L)
; :: thesis: 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;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

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