A1:
for x being object st x in dom hcflatplus holds

hcflatplus . x = hcflat . x

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

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

hcflatplus . x = hcflat . x

proof

( dom hcflatplus = [:NATPLUS,NATPLUS:] & dom hcflat = [:NAT,NAT:] )
by FUNCT_2:def 1;
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;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

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

( dom lcmlatplus = [:NATPLUS,NATPLUS:] & dom lcmlat = [:NAT,NAT:] )
by FUNCT_2:def 1;
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;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

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