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: hcflatplus . x = hcflat . x
then A3: x in [:NATPLUS,NATPLUS:] by FUNCT_2:def 1;
consider y1, y2 being object such that
A4: [y1,y2] = x by A2, RELAT_1:def 1;
( y1 in NATPLUS & y2 in NATPLUS ) by A3, A4, ZFMISC_1:87;
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 A3, A4, ZFMISC_1:87;
hcflatplus . (n,k) = hcflat . (n,k) by A5, Def8;
hence hcflatplus . x = hcflat . x by A4; :: thesis: verum

end;

( dom hcflatplus = [:NATPLUS,NATPLUS:] & dom hcflat = [:NAT,NAT:] ) by FUNCT_2:def 1;
then dom hcflatplus = (dom hcflat) /\ [:NATPLUS,NATPLUS:] by XBOOLE_1:28, ZFMISC_1:96;
then A6: hcflatplus = hcflat || NATPLUS by A1, FUNCT_1:46;
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: lcmlatplus . x = lcmlat . x
then A9: x in [:NATPLUS,NATPLUS:] by FUNCT_2:def 1;
consider y1, y2 being object such that
A10: [y1,y2] = x by A8, RELAT_1:def 1;
( y1 in NATPLUS & y2 in NATPLUS ) by A9, A10, ZFMISC_1:87;
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 A9, A10, ZFMISC_1:87;
lcmlatplus . (n,k) = lcmlat . (n,k) by A11, Def9;
hence lcmlatplus . x = lcmlat . x by A10; :: thesis: verum

end;

( dom lcmlatplus = [:NATPLUS,NATPLUS:] & dom lcmlat = [:NAT,NAT:] ) by FUNCT_2:def 1;
then dom lcmlatplus = (dom lcmlat) /\ [:NATPLUS,NATPLUS:] by XBOOLE_1:28, ZFMISC_1:96;
then lcmlatplus = lcmlat || NATPLUS by A7, FUNCT_1:46;
hence NatPlus_Lattice is SubLattice of Nat_Lattice by A6, Def12; :: thesis: verum