A1:
for x being object st x in dom hcflatplus holds
hcflatplus . x = hcflat . x
proof
let x be
object ;
( 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
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;
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: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
let x be
object ;
( 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
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;
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:96;
then
lcmlatplus = lcmlat || NATPLUS
by A7, FUNCT_1:46;
hence
NatPlus_Lattice is SubLattice of Nat_Lattice
by A6, Def12; verum