deffunc H₁( 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₁(x) from FUNCT_1:sch 3();

now :: thesis: for x being object st x in rng H holds
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;

then A5: rng H c= NAT ;
A6: rng (F +* H) c= (rng F) \/ (rng H) by FUNCT_4:17;
(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 ) )

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 ) )

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;

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

assume 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;

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: verum

end;

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 ) ) ; :: thesis: verum