A1: for x being object st x in dom hcflatplus holds
hcflatplus . x = hcflat . x
proof
let x be object ; :: thesis: ( x in dom hcflatplus implies hcflatplus . x = hcflat . x )
assume A2: x in dom hcflatplus ; :: thesis:
then A3: x in by FUNCT_2:def 1;
consider y1, y2 being object such that
A4: [y1,y2] = x by ;
( y1 in NATPLUS & y2 in NATPLUS ) by ;
then reconsider n = y1, k = y2 as Nat ;
A5: hcflat . (n,k) = n gcd k by Def1;
reconsider n = y1, k = y2 as NatPlus by ;
hcflatplus . (n,k) = hcflat . (n,k) by ;
hence hcflatplus . x = hcflat . x by A4; :: thesis: verum
end;
( dom hcflatplus = & dom hcflat = ) by FUNCT_2:def 1;
then dom hcflatplus = () /\ by ;
then A6: hcflatplus = hcflat || NATPLUS by ;
A7: for x being object st x in dom lcmlatplus holds
lcmlatplus . x = lcmlat . x
proof
let x be object ; :: thesis: ( x in dom lcmlatplus implies lcmlatplus . x = lcmlat . x )
assume A8: x in dom lcmlatplus ; :: thesis:
then A9: x in by FUNCT_2:def 1;
consider y1, y2 being object such that
A10: [y1,y2] = x by ;
( y1 in NATPLUS & y2 in NATPLUS ) by ;
then reconsider n = y1, k = y2 as Nat ;
A11: lcmlat . (n,k) = n lcm k by Def2;
reconsider n = y1, k = y2 as NatPlus by ;
lcmlatplus . (n,k) = lcmlat . (n,k) by ;
hence lcmlatplus . x = lcmlat . x by A10; :: thesis: verum
end;
( dom lcmlatplus = & dom lcmlat = ) by FUNCT_2:def 1;
then dom lcmlatplus = () /\ by ;
then lcmlatplus = lcmlat || NATPLUS by ;
hence NatPlus_Lattice is SubLattice of Nat_Lattice by ; :: thesis: verum