theorem LmEMDetX0: :: ZMODLAT2:28

for L being Z_Lattice holds ModuleStr(# the carrier of (EMLat L), the addF of (EMLat L), the ZeroF of (EMLat L), the lmult of (EMLat L) #) = EMbedding L