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 and
A4: x2 in dom f and
A5: f . x1 = f . x2 ; :: thesis:
reconsider k1 = x1, k2 = x2 as Element of NAT by A3, A4, FUNCT_2:def 1;
A6: f . k2 = k2 by A1;
f . k1 = k1 by A1;
hence x1 = x2 by A5, A6; :: thesis:

end;

A7: NAT c= rng f

proof

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

end;

rng f c= NAT by RELAT_1:def 19;
then rng f = NAT by A7, 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:
A9: f . k = k by A1;
reconsider k1 = k + 1 as Element of NAT by ORDINAL1:def 13;
A10: f . k1 = k1 by A1;
reconsider fk = f . k as Element of NAT ;
A11: SUCC (f . k),SCM+FSA = {(f . k),(succ fk)} by Th84;
hence f . (k + 1) in SUCC (f . k),SCM+FSA by A10, A9, TARSKI:def 2; :: thesis:
A12: dom f = NAT by FUNCT_2:def 1;
let j be Element of NAT ; :: thesis:
assume A13: f . j in SUCC (f . k),SCM+FSA ; :: thesis:
reconsider fk = f . k as Element of NAT ;

per cases by A11, A13, TARSKI:def 2;

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

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

end;

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

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

end;

end;