set hp = hcflatplus ;
set h = hcflat ;
set N = NATPLUS ;
[:NATPLUS,NATPLUS:] c= [:NAT,NAT:] ;
then A0: [:NATPLUS,NATPLUS:] c= dom hcflat by FUNCT_2:def 1;
hcflatplus = hcflat | [:NATPLUS,NATPLUS:]

proof

A1: dom hcflatplus = [:NATPLUS,NATPLUS:] by FUNCT_2:def 1
.= dom (hcflat | [:NATPLUS,NATPLUS:]) by RELAT_1:62, A0 ;
for x being object st x in dom hcflatplus holds
hcflatplus . x = (hcflat | [:NATPLUS,NATPLUS:]) . x

proof

let x be object ; :: thesis: ( x in dom hcflatplus implies hcflatplus . x = (hcflat | [:NATPLUS,NATPLUS:]) . x )
assume x in dom hcflatplus ; :: thesis: hcflatplus . x = (hcflat | [:NATPLUS,NATPLUS:]) . x
then A2: x in [:NATPLUS,NATPLUS:] by FUNCT_2:def 1;
then consider x1, x2 being object such that
B1: ( x1 in NATPLUS & x2 in NATPLUS & x = [x1,x2] ) by ZFMISC_1:def 2;
reconsider x1 = x1, x2 = x2 as NatPlus by B1;
thus hcflatplus . x = hcflatplus . (x1,x2) by B1
.= x1 gcd x2 by NAT_LAT:def 8
.= hcflat . (x1,x2) by NAT_LAT:def 1
.= (hcflat | [:NATPLUS,NATPLUS:]) . x by A2, FUNCT_1:49, B1 ; :: thesis: verum

end;

hence hcflatplus = hcflat | [:NATPLUS,NATPLUS:] by A1, FUNCT_1:2; :: thesis: verum

end;

hence hcflatplus = hcflat || NATPLUS ; :: thesis: verum