deffunc H₁( set ) -> Element of NAT = (F . $1) + k;
consider H being Function such that
A1: dom H = S /\ (dom F) and
A2: for x being set st x in S /\ (dom F) holds
H . x = H₁(x) from FUNCT_1:sch 3();

now

let x be set ; :: thesis: ( x in rng H implies x in NAT )
assume x in rng H ; :: thesis: x in NAT
then consider y being set 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; :: thesis: verum

end;

then A5: rng H c= NAT by TARSKI:def 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, XBOOLE_1:1;
then reconsider IT = F +* H as natural-valued Function by VALUED_0:def 6;
take IT ; :: thesis: ( dom IT = dom F & ( for y being set 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 set holds
( ( y in S & y in dom F implies IT . y = (F . y) + k ) & ( not y in S implies IT . y = F . y ) )

now

let y be set ; :: 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

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

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