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