let k be Nat; :: thesis:
let F be NAT -defined Function; :: thesis:
defpred S₁[ object , object ] means ex il being Element of NAT st
( $1 = il & $2 = k + il );
A1: for e being object st e in dom F holds
ex u being object st S₁[e,u]

let e be object ; :: thesis:
assume e in dom F ; :: thesis:
then reconsider e = e as Element of NAT ;
take k + e ; :: thesis:
take e ; :: thesis:
thus ( e = e & k + e = k + e ) ; :: thesis:

end;

consider f being Function such that
A2: dom f = dom F and
A3: for x being object st x in dom F holds
S₁[x,f . x] from CLASSES1:sch 1(A1);
take f ; :: according to WELLORD2:def 4 :: thesis:

hereby :: according to FUNCT_1:def 4 :: thesis:

let x1, x2 be object ; :: thesis:
assume that
A4: x1 in dom f and
A5: x2 in dom f and
A6: f . x1 = f . x2 ; :: thesis:
consider i1 being Element of NAT such that
A7: x1 = i1 and
A8: f . x1 = k + i1 by A2, A3, A4;
consider i2 being Element of NAT such that
A9: x2 = i2 and
A10: f . x2 = k + i2 by A2, A3, A5;
thus x1 = x2 by A7, A6, A8, A10, A9; :: thesis:

end;

thus dom f = dom F by A2; :: thesis:
A11: dom (Shift (F,k)) = { (m + k) where m is Nat : m in dom F } by Def12;

let y be object ; :: thesis:
assume y in rng f ; :: thesis:
then consider x being object such that
A12: x in dom f and
A13: f . x = y by FUNCT_1:def 3;
consider il being Element of NAT such that
A14: x = il and
A15: f . x = k + il by A2, A3, A12;
thus y in dom (Shift (F,k)) by A2, A11, A12, A13, A14, A15; :: thesis:

end;

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in dom (Shift (F,k)) ; :: thesis:
then consider m being Nat such that
A16: y = m + k and
A17: m in dom F by A11;
consider il being Element of NAT such that
A18: m = il and
A19: f . m = k + il by A3, A17;
thus y in rng f by A2, A16, A17, A18, A19, FUNCT_1:def 3; :: thesis: