let L be Z_Lattice; :: thesis: ModuleStr(# the carrier of (EMLat L), the addF of (EMLat L), the ZeroF of (EMLat L), the lmult of (EMLat L) #) = EMbedding L

Q1: the carrier of (EMLat L) = rng (MorphsZQ L) by defEMLat

.= the carrier of (EMbedding L) by ZMODUL08:def 3 ;

Q2: the ZeroF of (EMLat L) = zeroCoset L by defEMLat

.= the ZeroF of (EMbedding L) by ZMODUL08:def 3 ;

Q3: the addF of (EMLat L) = (addCoset L) || (rng (MorphsZQ L)) by defEMLat

.= the addF of (EMbedding L) by ZMODUL08:def 3 ;

Q4: the lmult of (EMLat L) = (lmultCoset L) | [: the carrier of INT.Ring,(rng (MorphsZQ L)):] by defEMLat

.= the lmult of (EMbedding L) by ZMODUL08:def 3 ;

thus ModuleStr(# the carrier of (EMLat L), the addF of (EMLat L), the ZeroF of (EMLat L), the lmult of (EMLat L) #) = EMbedding L by Q1, Q2, Q3, Q4; :: thesis: verum

Q1: the carrier of (EMLat L) = rng (MorphsZQ L) by defEMLat

.= the carrier of (EMbedding L) by ZMODUL08:def 3 ;

Q2: the ZeroF of (EMLat L) = zeroCoset L by defEMLat

.= the ZeroF of (EMbedding L) by ZMODUL08:def 3 ;

Q3: the addF of (EMLat L) = (addCoset L) || (rng (MorphsZQ L)) by defEMLat

.= the addF of (EMbedding L) by ZMODUL08:def 3 ;

Q4: the lmult of (EMLat L) = (lmultCoset L) | [: the carrier of INT.Ring,(rng (MorphsZQ L)):] by defEMLat

.= the lmult of (EMbedding L) by ZMODUL08:def 3 ;

thus ModuleStr(# the carrier of (EMLat L), the addF of (EMLat L), the ZeroF of (EMLat L), the lmult of (EMLat L) #) = EMbedding L by Q1, Q2, Q3, Q4; :: thesis: verum