let L be Z_Lattice; :: thesis: EMLat L is Submodule of DivisibleMod L
A1: the carrier of (EMbedding L) = rng (MorphsZQ L) by ZMODUL08:def 3
.= the carrier of (EMLat L) by defEMLat ;
A2: the addF of (EMLat L) = (addCoset L) || (rng (MorphsZQ L)) by defEMLat
.= the addF of (EMbedding L) by ZMODUL08:def 3 ;
then reconsider ad = the addF of (EMbedding L) as BinOp of the carrier of (EMLat L) ;
A3: 0. (EMbedding L) = zeroCoset L by ZMODUL08:def 3
.= 0. (EMLat L) by defEMLat ;
then reconsider ze = 0. (EMbedding L) as Vector of (EMLat L) ;
A4: 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 ;
then reconsider mu = the lmult of (EMbedding L) as Function of [: the carrier of INT.Ring, the carrier of (EMLat L):], the carrier of (EMLat L) ;
reconsider sc = the scalar of (EMLat L) as Function of [: the carrier of (EMbedding L), the carrier of (EMbedding L):], the carrier of F_Real by A1;
EMLat L = GenLat ((EMbedding L),sc) by A1, A2, A3, A4;
then A2: EMLat L is Submodule of EMbedding L by ZMODLAT1:2;
EMbedding L is Submodule of DivisibleMod L by ZMODUL08:24;
hence EMLat L is Submodule of DivisibleMod L by A2, ZMODUL01:42; :: thesis: verum