let f be Function of NAT ,NAT ; :: thesis:
assume A1: for k being Element of NAT holds f . k = k ; :: thesis:
A2: f is one-to-one

proof

let x1, x2 be set ; :: according to FUNCT_1:def 8 :: thesis:
assume that
A3: ( x1 in dom f & x2 in dom f ) and
A4: f . x1 = f . x2 ; :: thesis:
reconsider k1 = x1, k2 = x2 as Element of NAT by A3, FUNCT_2:def 1;
( f . k1 = k1 & f . k2 = k2 ) by A1;
hence x1 = x2 by A4; :: thesis:

end;

A5: NAT c= rng f

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in NAT ; :: thesis:
then reconsider i = x as Element of NAT ;
( dom f = NAT & i = f . i ) by A1, FUNCT_2:def 1;
hence x in rng f by FUNCT_1:def 5; :: thesis:

end;

rng f c= NAT by RELAT_1:def 19;
then rng f = NAT by A5, XBOOLE_0:def 10;
then f is onto by FUNCT_2:def 3;
hence f is bijective by A2; :: thesis:
let k be Element of NAT ; :: thesis:
A6: f . k = k by A1;
k + 1 in NAT by ORDINAL1:def 13;
then A7: f . (k + 1) = k + 1 by A1;
reconsider fk = f . k as Element of NAT ;
A8: SUCC (f . k),SCM = {(f . k),(succ fk)} by Th52;
hence f . (k + 1) in SUCC (f . k),SCM by A7, A6, TARSKI:def 2; :: thesis:
A9: dom f = NAT by FUNCT_2:def 1;
let j be Element of NAT ; :: thesis:
assume A10: f . j in SUCC (f . k),SCM ; :: thesis:
reconsider fk = f . k as Element of NAT ;

per cases by A8, A10, TARSKI:def 2;

suppose f . j = f . k ; :: thesis:

hence k <= j by A2, A9, FUNCT_1:def 8; :: thesis:

end;

suppose f . j = succ fk ; :: thesis:

then j = k + 1 by A2, A7, A6, A9, FUNCT_1:def 8;
hence k <= j by NAT_1:11; :: thesis:

end;

end;