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

proof

let e be set ; :: thesis: ( e in dom F implies ex u being set st S₁[e,u] )
assume e in dom F ; :: thesis: ex u being set st S₁[e,u]
then reconsider e = e as Element of NAT by A1;
take k + e ; :: thesis: S₁[e,k + e]
take e ; :: thesis: ( e = e & k + e = k + e )
thus ( e = e & k + e = k + e ) ; :: thesis: verum

end;

consider f being Function such that
A3: dom f = dom F and
A4: for x being set st x in dom F holds
S₁[x,f . x] from CLASSES1:sch 1(A2);
take f ; :: according to WELLORD2:def 4 :: thesis: ( f is one-to-one & proj1 f = dom F & proj2 f = dom (Shift (F,k)) )

hereby :: according to FUNCT_1:def 4 :: thesis: ( proj1 f = dom F & proj2 f = dom (Shift (F,k)) )

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

end;

thus dom f = dom F by A3; :: thesis: proj2 f = dom (Shift (F,k))
A12: dom (Shift (F,k)) = { (m + k) where m is Element of NAT : m in dom F } by Def12;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: dom (Shift (F,k)) c= proj2 f

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

end;

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in dom (Shift (F,k)) or y in proj2 f )
assume y in dom (Shift (F,k)) ; :: thesis: y in proj2 f
then consider m being Element of NAT such that
A17: y = m + k and
A18: m in dom F by A12;
consider il being Element of NAT such that
A19: m = il and
A20: f . m = k + il by A4, A18;
thus y in proj2 f by A3, A17, A18, A19, A20, FUNCT_1:def 3; :: thesis: verum