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