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 ; :: thesis: ( x in dom lcmlatplus implies lcmlatplus . x = (lcmlat | [:NATPLUS,NATPLUS:]) . x )
assume x in dom lcmlatplus ; :: thesis: 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 ; :: thesis: verum

end;

hence lcmlatplus = lcmlat | [:NATPLUS,NATPLUS:] by A1, FUNCT_1:2; :: thesis: verum

end;

hence lcmlatplus = lcmlat || NATPLUS ; :: thesis: verum