let L be Z_Lattice; :: thesis: for I being Subset of L holds
( I is Basis of L iff (MorphsZQ L) .: I is Basis of (EMLat L) )
let I be Subset of L; :: thesis: ( I is Basis of L iff (MorphsZQ L) .: I is Basis of (EMLat L) )
P1: ( I is Basis of L iff (MorphsZQ L) .: I is Basis of (EMbedding L) ) by LmEMDetX6;
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 LmEMDetX0;
hence ( I is Basis of L iff (MorphsZQ L) .: I is Basis of (EMLat L) ) by P1, LmEMDetX5; :: thesis: verum