reconsider ad = the addF of (DivisibleMod L) || (DualSet L) as Function of [:(DualSet L),(DualSet L):], the carrier of (DivisibleMod L) by FUNCT_2:32;
for z being Element of [:(DualSet L),(DualSet L):] holds ad . z in DualSet L

proof

let z be Element of [:(DualSet L),(DualSet L):]; :: thesis: ad . z in DualSet L
consider x, y being object such that
G1: ( x in DualSet L & y in DualSet L & z = [x,y] ) by ZFMISC_1:def 2;
reconsider x = x, y = y as Element of (DivisibleMod L) by G1;
ad . z = x + y by FUNCT_1:49, G1;
hence ad . z in DualSet L by G1, VECTSP_4:def 1; :: thesis: verum

end;

then rng ad c= DualSet L by FUNCT_2:114;
then reconsider ad = ad as BinOp of (DualSet L) by FUNCT_2:6;
0. (DivisibleMod L) is Dual of L by LmDE0;
then 0. (DivisibleMod L) in DualSet L ;
then reconsider ze = 0. (DivisibleMod L) as Element of DualSet L ;
[: the carrier of INT.Ring,(DualSet L):] c= [: the carrier of INT.Ring, the carrier of (DivisibleMod L):] by ZFMISC_1:95;
then reconsider mu = the lmult of (DivisibleMod L) | [: the carrier of INT.Ring,(DualSet L):] as Function of [: the carrier of INT.Ring,(DualSet L):], the carrier of (DivisibleMod L) by FUNCT_2:32;
for z being Element of [: the carrier of INT.Ring,(DualSet L):] holds mu . z in DualSet L

proof

let z be Element of [: the carrier of INT.Ring,(DualSet L):]; :: thesis: mu . z in DualSet L
consider x, y being object such that
G1: ( x in the carrier of INT.Ring & y in DualSet L & z = [x,y] ) by ZFMISC_1:def 2;
reconsider x = x as Element of INT.Ring by G1;
reconsider y = y as Element of (DivisibleMod L) by G1;
mu . z = x * y by FUNCT_1:49, G1;
hence mu . z in DualSet L by G1, VECTSP_4:def 1; :: thesis: verum

end;

then rng mu c= DualSet L by FUNCT_2:114;
then reconsider mu = mu as Function of [: the carrier of INT.Ring,(DualSet L):],(DualSet L) by FUNCT_2:6;
reconsider sc = (ScProductDM L) | [:(DualSet L),(DualSet L):] as Function of [:(DualSet L),(DualSet L):], the carrier of F_Real by FUNCT_2:32;
take IT = LatticeStr(# (DualSet L),ad,ze,mu,sc #); :: thesis: ( the carrier of IT = DualSet L & the addF of IT = the addF of (DivisibleMod L) || (DualSet L) & the ZeroF of IT = 0. (DivisibleMod L) & the lmult of IT = the lmult of (DivisibleMod L) | [: the carrier of INT.Ring,(DualSet L):] & the scalar of IT = (ScProductDM L) | [:(DualSet L),(DualSet L):] )
thus ( the carrier of IT = DualSet L & the addF of IT = the addF of (DivisibleMod L) || (DualSet L) & the ZeroF of IT = 0. (DivisibleMod L) & the lmult of IT = the lmult of (DivisibleMod L) | [: the carrier of INT.Ring,(DualSet L):] & the scalar of IT = (ScProductDM L) | [:(DualSet L),(DualSet L):] ) ; :: thesis: verum