let L be Z_Lattice; :: thesis: 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 )
let E be free finite-rank Z_Module; :: thesis: 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 )
let I be FinSequence of L; :: thesis: 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 )
let J be FinSequence of E; :: thesis: ( 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 implies ( I is OrdBasis of L iff J is OrdBasis of E ) )
assume that
AS1: 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 #) and
AS2: I = J ; :: thesis: ( I is OrdBasis of L iff J is OrdBasis of E )
hereby :: thesis: ( J is OrdBasis of E implies I is OrdBasis of L )
assume I is OrdBasis of L ; :: thesis: J is OrdBasis of E
then P2: ( I is one-to-one & rng I is Basis of L ) by ZMATRLIN:def 5;
then rng J is Basis of E by AS1, AS2, LmEMDetX5;
hence J is OrdBasis of E by AS2, P2, ZMATRLIN:def 5; :: thesis: verum
end;
assume J is OrdBasis of E ; :: thesis: I is OrdBasis of L
then P2: ( J is one-to-one & rng J is Basis of E ) by ZMATRLIN:def 5;
then rng I is Basis of L by AS1, AS2, LmEMDetX5;
hence I is OrdBasis of L by AS2, P2, ZMATRLIN:def 5; :: thesis: verum