theorem LmEMDetX4: :: ZMODLAT2:36

for L, E being free finite-rank Z_Module 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 #) holds
rank L = rank E