let L, E be free Z_Module; 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; 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; ( 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
; ( I is Basis of L iff J is Basis of E )
hereby ( J is Basis of E implies I is Basis of L )
assume P1:
I is
Basis of
L
;
J is Basis of Ethen
(
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;
verum
end;
assume P1:
J is Basis of E
; 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 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; verum