let L be Z_Lattice; 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; verum