reconsider ad = the addF of () || () as Function of [:(),():], the carrier of () by FUNCT_2:32;
for z being Element of [:(),():] holds ad . z in DualSet L
proof
let z be Element of [:(),():]; :: 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 () by G1;
ad . z = x + y by ;
hence ad . z in DualSet L by ; :: thesis: verum
end;
then rng ad c= DualSet L by FUNCT_2:114;
0. () is Dual of L by LmDE0;
then 0. () in DualSet L ;
then reconsider ze = 0. () as Element of DualSet L ;
[: the carrier of INT.Ring,():] c= [: the carrier of INT.Ring, the carrier of ():] by ZFMISC_1:95;
then reconsider mu = the lmult of () | [: the carrier of INT.Ring,():] as Function of [: the carrier of INT.Ring,():], the carrier of () by FUNCT_2:32;
for z being Element of [: the carrier of INT.Ring,():] holds mu . z in DualSet L
proof
let z be Element of [: the carrier of INT.Ring,():]; :: 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 () by G1;
mu . z = x * y by ;
hence mu . z in DualSet L by ; :: 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,():],() by FUNCT_2:6;
reconsider sc = () | [:(),():] as Function of [:(),():], the carrier of F_Real by FUNCT_2:32;
take IT = LatticeStr(# (),ad,ze,mu,sc #); :: thesis: ( the carrier of IT = DualSet L & the addF of IT = the addF of () || () & the ZeroF of IT = 0. () & the lmult of IT = the lmult of () | [: the carrier of INT.Ring,():] & the scalar of IT = () | [:(),():] )
thus ( the carrier of IT = DualSet L & the addF of IT = the addF of () || () & the ZeroF of IT = 0. () & the lmult of IT = the lmult of () | [: the carrier of INT.Ring,():] & the scalar of IT = () | [:(),():] ) ; :: thesis: verum