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

( 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