let L be Z_Lattice; :: thesis: for I being Basis of (EMLat L) holds I is Basis of (EMbedding L)
let I be Basis of (EMLat L); :: thesis: I is Basis of (EMbedding L)
ModuleStr(# the carrier of (EMLat L), the addF of (EMLat L), the ZeroF of (EMLat L), the lmult of (EMLat L) #) = ModuleStr(# the carrier of (EMbedding L), the addF of (EMbedding L), the ZeroF of (EMbedding L), the lmult of (EMbedding L) #) by ZMODLAT2:28;
hence I is Basis of (EMbedding L) by ZMODLAT2:35; :: thesis: verum