set hp = lcmlatplus ;
set h = lcmlat ;
set N = NATPLUS ;
[:NATPLUS,NATPLUS:] c= [:NAT,NAT:]
;
then A0:
[:NATPLUS,NATPLUS:] c= dom lcmlat
by FUNCT_2:def 1;
lcmlatplus = lcmlat | [:NATPLUS,NATPLUS:]
proof
A1:
dom lcmlatplus =
[:NATPLUS,NATPLUS:]
by FUNCT_2:def 1
.=
dom (lcmlat | [:NATPLUS,NATPLUS:])
by RELAT_1:62, A0
;
for
x being
object st
x in dom lcmlatplus holds
lcmlatplus . x = (lcmlat | [:NATPLUS,NATPLUS:]) . x
proof
let x be
object ;
( x in dom lcmlatplus implies lcmlatplus . x = (lcmlat | [:NATPLUS,NATPLUS:]) . x )
assume
x in dom lcmlatplus
;
lcmlatplus . x = (lcmlat | [: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 lcmlatplus . x =
lcmlatplus . (
x1,
x2)
by B1
.=
x1 lcm x2
by NAT_LAT:def 9
.=
lcmlat . (
x1,
x2)
by NAT_LAT:def 2
.=
(lcmlat | [:NATPLUS,NATPLUS:]) . x
by A2, FUNCT_1:49, B1
;
verum
end;
hence
lcmlatplus = lcmlat | [:NATPLUS,NATPLUS:]
by A1, FUNCT_1:2;
verum
end;
hence
lcmlatplus = lcmlat || NATPLUS
; verum