let R be good Ring; :: thesis: for k being natural number holds il. (SCM R),k = k
let k be natural number ; :: thesis: il. (SCM R),k = k
deffunc H₁( Element of NAT ) -> Element of NAT = $1;
A1: for x being Element of NAT holds H₁(x) is Element of NAT ;
consider f being Function of NAT ,NAT such that
A2: for k being Element of NAT holds f . k = H₁(k) from FUNCT_2:sch 9(A1);
reconsider f = f as Function of NAT ,NAT ;
A3: ( f is bijective & ( for k being Element of NAT holds
( f . (k + 1) in SUCC (f . k),(SCM R) & ( for j being Element of NAT st f . j in SUCC (f . k),(SCM R) holds
k <= j ) ) ) ) by A2, Th65;
ex f being Function of NAT ,NAT st
( f is bijective & ( for m, n being Element of NAT holds
( m <= n iff f . m <= f . n, SCM R ) ) & k = f . k )

proof

take f ; :: thesis: ( f is bijective & ( for m, n being Element of NAT holds
( m <= n iff f . m <= f . n, SCM R ) ) & k = f . k )
thus f is bijective by A2, Th65; :: thesis: ( ( for m, n being Element of NAT holds
( m <= n iff f . m <= f . n, SCM R ) ) & k = f . k )
thus for m, n being Element of NAT holds
( m <= n iff f . m <= f . n, SCM R ) by A3, AMISTD_1:18; :: thesis: k = f . k
k in NAT by ORDINAL1:def 13;
hence k = f . k by A2; :: thesis: verum

end;

then consider f being Function of NAT ,NAT such that
W: ( f is bijective & ( for m, n being Element of NAT holds
( m <= n iff f . m <= f . n, SCM R ) ) & k = f . k ) ;
reconsider l = k as Element of NAT by ORDINAL1:def 13;
ex f being Function of NAT ,NAT st
( f is bijective & ( for m, n being Element of NAT holds
( m <= n iff f . m <= f . n, SCM R ) ) & l = f . k ) by W;
then l = il. (SCM R),k by AMISTD_1:def 12;
hence il. (SCM R),k = k ; :: thesis: verum