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 )
hereby :: thesis: ( J is Basis of E implies I is Basis of L )
assume 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 ;
Lin J = Lin I by
.= ModuleStr(# the carrier of E, the addF of E, the ZeroF of E, the lmult of E #) by ;
hence J is Basis of E by ; :: thesis: verum
end;
assume P1: J is Basis of E ; :: thesis: I is Basis of L
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 ;
Lin I = Lin J by
.= ModuleStr(# the carrier of L, the addF of L, the ZeroF of L, the lmult of L #) by ;
hence I is Basis of L by ; :: thesis: verum