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

proof

let e be object ; :: thesis: ( e in dom F implies ex u being object st S₁[e,u] )
assume e in dom F ; :: thesis: ex u being object st S₁[e,u]
then reconsider e = e as Element of NAT ;
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
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: ( f is one-to-one & dom f = dom F & rng f = dom (Shift (F,k)) )

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

let x1, x2 be object ; :: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume that
A4: x1 in dom f and
A5: x2 in dom f and
A6: f . x1 = f . x2 ; :: thesis: x1 = x2
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: verum

end;

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

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

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

end;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in dom (Shift (F,k)) or y in rng f )
assume y in dom (Shift (F,k)) ; :: thesis: y in rng f
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: verum