deffunc H_{1}( object ) -> set = (F . $1) + k;

consider H being Function such that

A1: dom H = S /\ (dom F) and

A2: for x being object st x in S /\ (dom F) holds

H . x = H_{1}(x)
from FUNCT_1:sch 3();

A6: rng (F +* H) c= (rng F) \/ (rng H) by FUNCT_4:17;

rng F c= NAT by VALUED_0:def 6;

then (rng F) \/ (rng H) c= NAT by A5, XBOOLE_1:8;

then rng (F +* H) c= NAT by A6;

then reconsider IT = F +* H as natural-valued Function by VALUED_0:def 6;

take IT ; :: thesis: ( dom IT = dom F & ( for y being object holds

( ( y in S & y in dom F implies IT . y = (F . y) + k ) & ( not y in S implies IT . y = F . y ) ) ) )

dom IT = (dom F) \/ (S /\ (dom F)) by A1, FUNCT_4:def 1;

hence dom IT = dom F by XBOOLE_1:22; :: thesis: for y being object holds

( ( y in S & y in dom F implies IT . y = (F . y) + k ) & ( not y in S implies IT . y = F . y ) )

( ( y in S & y in dom F implies IT . y = (F . y) + k ) & ( not y in S implies IT . y = F . y ) ) ; :: thesis: verum

consider H being Function such that

A1: dom H = S /\ (dom F) and

A2: for x being object st x in S /\ (dom F) holds

H . x = H

now :: thesis: for x being object st x in rng H holds

x in NAT

then A5:
rng H c= NAT
;x in NAT

let x be object ; :: thesis: ( x in rng H implies x in NAT )

assume x in rng H ; :: thesis: x in NAT

then consider y being object such that

A3: y in dom H and

A4: H . y = x by FUNCT_1:def 3;

H . y = (F . y) + k by A1, A2, A3;

hence x in NAT by A4, ORDINAL1:def 12; :: thesis: verum

end;assume x in rng H ; :: thesis: x in NAT

then consider y being object such that

A3: y in dom H and

A4: H . y = x by FUNCT_1:def 3;

H . y = (F . y) + k by A1, A2, A3;

hence x in NAT by A4, ORDINAL1:def 12; :: thesis: verum

A6: rng (F +* H) c= (rng F) \/ (rng H) by FUNCT_4:17;

rng F c= NAT by VALUED_0:def 6;

then (rng F) \/ (rng H) c= NAT by A5, XBOOLE_1:8;

then rng (F +* H) c= NAT by A6;

then reconsider IT = F +* H as natural-valued Function by VALUED_0:def 6;

take IT ; :: thesis: ( dom IT = dom F & ( for y being object holds

( ( y in S & y in dom F implies IT . y = (F . y) + k ) & ( not y in S implies IT . y = F . y ) ) ) )

dom IT = (dom F) \/ (S /\ (dom F)) by A1, FUNCT_4:def 1;

hence dom IT = dom F by XBOOLE_1:22; :: thesis: for y being object holds

( ( y in S & y in dom F implies IT . y = (F . y) + k ) & ( not y in S implies IT . y = F . y ) )

now :: thesis: for y being object holds

( ( y in S & y in dom F implies IT . y = (F . y) + k ) & ( not y in S implies IT . y = F . y ) )

hence
for y being object holds ( ( y in S & y in dom F implies IT . y = (F . y) + k ) & ( not y in S implies IT . y = F . y ) )

let y be object ; :: thesis: ( ( y in S & y in dom F implies IT . y = (F . y) + k ) & ( not y in S implies IT . y = F . y ) )

end;A7: now :: thesis: ( y in S & y in dom F implies IT . y = (F . y) + k )

assume that

A8: y in S and

A9: y in dom F ; :: thesis: IT . y = (F . y) + k

y in dom H by A1, A8, A9, XBOOLE_0:def 4;

then A10: IT . y = H . y by FUNCT_4:13;

y in S /\ (dom F) by A8, A9, XBOOLE_0:def 4;

hence IT . y = (F . y) + k by A2, A10; :: thesis: verum

end;A8: y in S and

A9: y in dom F ; :: thesis: IT . y = (F . y) + k

y in dom H by A1, A8, A9, XBOOLE_0:def 4;

then A10: IT . y = H . y by FUNCT_4:13;

y in S /\ (dom F) by A8, A9, XBOOLE_0:def 4;

hence IT . y = (F . y) + k by A2, A10; :: thesis: verum

now :: thesis: ( not y in S implies IT . y = F . y )

hence
( ( y in S & y in dom F implies IT . y = (F . y) + k ) & ( not y in S implies IT . y = F . y ) )
by A7; :: thesis: verumassume
not y in S
; :: thesis: IT . y = F . y

then not y in dom H by A1, XBOOLE_0:def 4;

hence IT . y = F . y by FUNCT_4:11; :: thesis: verum

end;then not y in dom H by A1, XBOOLE_0:def 4;

hence IT . y = F . y by FUNCT_4:11; :: thesis: verum

( ( y in S & y in dom F implies IT . y = (F . y) + k ) & ( not y in S implies IT . y = F . y ) ) ; :: thesis: verum