theorem LmEMDetX9: :: ZMODLAT2:40

for L being Z_Lattice
for E being free finite-rank Z_Module
for I being FinSequence of L
for J being FinSequence of E st ModuleStr(# the carrier of L, the addF of L, the ZeroF of L, the lmult of L #) = ModuleStr(# the carrier of E, the addF of E, the ZeroF of E, the lmult of E #) & I = J holds
( I is OrdBasis of L iff J is OrdBasis of E )