A1:
for x being set st x in dom hcflatplus holds
hcflatplus . x = hcflat . x
proof
let x be
set ;
( x in dom hcflatplus implies hcflatplus . x = hcflat . x )
assume A2:
x in dom hcflatplus
;
hcflatplus . x = hcflat . x
then A3:
x in [:NATPLUS ,NATPLUS :]
by FUNCT_2:def 1;
consider y1,
y2 being
set such that A4:
[y1,y2] = x
by A2, RELAT_1:def 1;
(
y1 in NATPLUS &
y2 in NATPLUS )
by A3, A4, ZFMISC_1:106;
then reconsider n =
y1,
k =
y2 as
Nat ;
A5:
hcflat . n,
k = n gcd k
by Def3;
reconsider n =
y1,
k =
y2 as
NatPlus by A3, A4, ZFMISC_1:106;
hcflatplus . n,
k = hcflat . n,
k
by A5, Def12;
hence
hcflatplus . x = hcflat . x
by A4;
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:119;
then A6:
hcflatplus = hcflat || NATPLUS
by A1, FUNCT_1:68;
A7:
for x being set st x in dom lcmlatplus holds
lcmlatplus . x = lcmlat . x
proof
let x be
set ;
( x in dom lcmlatplus implies lcmlatplus . x = lcmlat . x )
assume A8:
x in dom lcmlatplus
;
lcmlatplus . x = lcmlat . x
then A9:
x in [:NATPLUS ,NATPLUS :]
by FUNCT_2:def 1;
consider y1,
y2 being
set such that A10:
[y1,y2] = x
by A8, RELAT_1:def 1;
(
y1 in NATPLUS &
y2 in NATPLUS )
by A9, A10, ZFMISC_1:106;
then reconsider n =
y1,
k =
y2 as
Nat ;
A11:
lcmlat . n,
k = n lcm k
by Def4;
reconsider n =
y1,
k =
y2 as
NatPlus by A9, A10, ZFMISC_1:106;
lcmlatplus . n,
k = lcmlat . n,
k
by A11, Def13;
hence
lcmlatplus . x = lcmlat . x
by A10;
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:119;
then
lcmlatplus = lcmlat || NATPLUS
by A7, FUNCT_1:68;
hence
NatPlus_Lattice is SubLattice of Nat_Lattice
by A6, Def16; verum