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 )

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

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
J is OrdBasis of E
; :: thesis: I is OrdBasis of Lassume
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;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

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