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