let L, E be free finite-rank Z_Module; ( 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 #) implies rank L = rank E )
assume AS:
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 #)
; rank L = rank E
set I = the Basis of L;
P1:
rank L = card the Basis of L
by ZMODUL03:def 5;
reconsider J = the Basis of L as Subset of E by AS;
J is Basis of E
by LmEMDetX5, AS;
hence
rank L = rank E
by P1, ZMODUL03:def 5; verum