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 ;
( x in dom hcflatplus implies hcflatplus . x = (hcflat | [:NATPLUS,NATPLUS:]) . x )
assume
x in dom hcflatplus
;
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
;
verum
end;
hence
hcflatplus = hcflat | [:NATPLUS,NATPLUS:]
by A1, FUNCT_1:2;
verum
end;
hence
hcflatplus = hcflat || NATPLUS
; verum