let L be Z_Lattice; :: thesis: for b being FinSequence of L holds

( b is OrdBasis of L iff (MorphsZQ L) * b is OrdBasis of EMLat L )

let b be FinSequence of L; :: thesis: ( b is OrdBasis of L iff (MorphsZQ L) * b is OrdBasis of EMLat L )

P1: ( b is OrdBasis of L iff (MorphsZQ L) * b is OrdBasis of EMbedding L ) by LmEMDetX8;

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 ( b is OrdBasis of L iff (MorphsZQ L) * b is OrdBasis of EMLat L ) by P1, LmEMDetX9; :: thesis: verum

( b is OrdBasis of L iff (MorphsZQ L) * b is OrdBasis of EMLat L )

let b be FinSequence of L; :: thesis: ( b is OrdBasis of L iff (MorphsZQ L) * b is OrdBasis of EMLat L )

P1: ( b is OrdBasis of L iff (MorphsZQ L) * b is OrdBasis of EMbedding L ) by LmEMDetX8;

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 ( b is OrdBasis of L iff (MorphsZQ L) * b is OrdBasis of EMLat L ) by P1, LmEMDetX9; :: thesis: verum