let R be good Ring; :: thesis:
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 l = x as Element of NAT ;
reconsider i = l 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 NAT = rng f 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 + 1) = k + 1 & f . k = k ) by A1;
reconsider fk = f . k as Element of NAT ;
A7: SUCC (f . k),(SCM R) = {(f . k),(succ fk)} by Th64;
hence f . (k + 1) in SUCC (f . k),(SCM R) by A6, TARSKI:def 2; :: thesis:
let j be Element of NAT ; :: thesis:
A8: dom f = NAT by FUNCT_2:def 1;
assume A9: f . j in SUCC (f . k),(SCM R) ; :: thesis:
reconsider fk = f . k as Element of NAT ;

per cases by A7, A9, TARSKI:def 2;

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

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

end;

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

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

end;

end;