let L, E be free finite-rank Z_Module; :: 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 #) 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 #) ; :: thesis: 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; :: thesis: verum

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 #) ; :: thesis: 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; :: thesis: verum