let L, E be free Z_Module; :: thesis: for I being Subset of L

for J being Subset 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 Basis of L iff J is Basis of E )

let I be Subset of L; :: thesis: for J being Subset 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 Basis of L iff J is Basis of E )

let J be Subset 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 Basis of L iff J is Basis of E ) )

assume that

A1: 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

A2: I = J ; :: thesis: ( I is Basis of L iff J is Basis of E )

then ( J is linearly-independent & Lin J = ModuleStr(# the carrier of E, the addF of E, the ZeroF of E, the lmult of E #) ) by VECTSP_7:def 3;

then P2: I is linearly-independent by A1, A2, LmEMDetX51;

Lin I = Lin J by A1, A2, LmEMDetX52

.= ModuleStr(# the carrier of L, the addF of L, the ZeroF of L, the lmult of L #) by A1, P1, VECTSP_7:def 3 ;

hence I is Basis of L by P2, VECTSP_7:def 3; :: thesis: verum

for J being Subset 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 Basis of L iff J is Basis of E )

let I be Subset of L; :: thesis: for J being Subset 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 Basis of L iff J is Basis of E )

let J be Subset 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 Basis of L iff J is Basis of E ) )

assume that

A1: 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

A2: I = J ; :: thesis: ( I is Basis of L iff J is Basis of E )

hereby :: thesis: ( J is Basis of E implies I is Basis of L )

assume P1:
J is Basis of E
; :: thesis: I is Basis of Lassume P1:
I is Basis of L
; :: thesis: J is Basis of E

then ( I is linearly-independent & Lin I = ModuleStr(# the carrier of L, the addF of L, the ZeroF of L, the lmult of L #) ) by VECTSP_7:def 3;

then P2: J is linearly-independent by A1, A2, LmEMDetX51;

Lin J = Lin I by A1, A2, LmEMDetX52

.= ModuleStr(# the carrier of E, the addF of E, the ZeroF of E, the lmult of E #) by A1, P1, VECTSP_7:def 3 ;

hence J is Basis of E by P2, VECTSP_7:def 3; :: thesis: verum

end;then ( I is linearly-independent & Lin I = ModuleStr(# the carrier of L, the addF of L, the ZeroF of L, the lmult of L #) ) by VECTSP_7:def 3;

then P2: J is linearly-independent by A1, A2, LmEMDetX51;

Lin J = Lin I by A1, A2, LmEMDetX52

.= ModuleStr(# the carrier of E, the addF of E, the ZeroF of E, the lmult of E #) by A1, P1, VECTSP_7:def 3 ;

hence J is Basis of E by P2, VECTSP_7:def 3; :: thesis: verum

then ( J is linearly-independent & Lin J = ModuleStr(# the carrier of E, the addF of E, the ZeroF of E, the lmult of E #) ) by VECTSP_7:def 3;

then P2: I is linearly-independent by A1, A2, LmEMDetX51;

Lin I = Lin J by A1, A2, LmEMDetX52

.= ModuleStr(# the carrier of L, the addF of L, the ZeroF of L, the lmult of L #) by A1, P1, VECTSP_7:def 3 ;

hence I is Basis of L by P2, VECTSP_7:def 3; :: thesis: verum