A1: lcmlatplus = lcmlat || NATPLUS

proof

A2: dom lcmlatplus = (dom lcmlat ) /\ [:NATPLUS ,NATPLUS :]

proof

A3: dom lcmlatplus = [:NATPLUS ,NATPLUS :] by FUNCT_2:def 1;
dom lcmlat = [:NAT ,NAT :] by FUNCT_2:def 1;
hence dom lcmlatplus = (dom lcmlat ) /\ [:NATPLUS ,NATPLUS :] by A3, XBOOLE_1:28, ZFMISC_1:119; :: thesis: verum

end;

for x being set st x in dom lcmlatplus holds
lcmlatplus . x = lcmlat . x

proof

let x be set ; :: thesis: ( x in dom lcmlatplus implies lcmlatplus . x = lcmlat . x )
assume A4: x in dom lcmlatplus ; :: thesis: lcmlatplus . x = lcmlat . x
then A5: x in [:NATPLUS ,NATPLUS :] by FUNCT_2:def 1;
consider y1, y2 being set such that
A6: [y1,y2] = x by A4, RELAT_1:def 1;
( y1 in NATPLUS & y2 in NATPLUS ) by A5, A6, ZFMISC_1:106;
then reconsider n = y1, k = y2 as Nat ;
A7: lcmlat . n,k = n lcm k by Def4;
reconsider n = y1, k = y2 as NatPlus by A5, A6, ZFMISC_1:106;
lcmlatplus . n,k = lcmlat . n,k by A7, Def13;
hence lcmlatplus . x = lcmlat . x by A6; :: thesis: verum

end;

hence lcmlatplus = lcmlat || NATPLUS by A2, FUNCT_1:68; :: thesis: verum

end;

hcflatplus = hcflat || NATPLUS

proof

A8: dom hcflatplus = (dom hcflat ) /\ [:NATPLUS ,NATPLUS :]

proof

A9: dom hcflatplus = [:NATPLUS ,NATPLUS :] by FUNCT_2:def 1;
dom hcflat = [:NAT ,NAT :] by FUNCT_2:def 1;
hence dom hcflatplus = (dom hcflat ) /\ [:NATPLUS ,NATPLUS :] by A9, XBOOLE_1:28, ZFMISC_1:119; :: thesis: verum

end;

for x being set st x in dom hcflatplus holds
hcflatplus . x = hcflat . x

proof

let x be set ; :: thesis: ( x in dom hcflatplus implies hcflatplus . x = hcflat . x )
assume A10: x in dom hcflatplus ; :: thesis: hcflatplus . x = hcflat . x
then A11: x in [:NATPLUS ,NATPLUS :] by FUNCT_2:def 1;
consider y1, y2 being set such that
A12: [y1,y2] = x by A10, RELAT_1:def 1;
( y1 in NATPLUS & y2 in NATPLUS ) by A11, A12, ZFMISC_1:106;
then reconsider n = y1, k = y2 as Nat ;
A13: hcflat . n,k = n gcd k by Def3;
reconsider n = y1, k = y2 as NatPlus by A11, A12, ZFMISC_1:106;
hcflatplus . n,k = hcflat . n,k by A13, Def12;
hence hcflatplus . x = hcflat . x by A12; :: thesis: verum

end;

hence hcflatplus = hcflat || NATPLUS by A8, FUNCT_1:68; :: thesis: verum

end;

hence NatPlus_Lattice is SubLattice of Nat_Lattice by A1, Def16; :: thesis: verum