let z be Nat; :: thesis: for N being with_zero set holds il. ((STC N),z) = z
let N be with_zero set ; :: thesis: il. ((STC N),z) = z
set M = STC N;
reconsider f2 = id NAT as sequence of NAT ;
consider f being sequence of NAT such that
A1: ( f is bijective & ( for m, n being Element of NAT holds
( m <= n iff f . m <= f . n, STC N ) ) ) and
A2: il. ((STC N),z) = f . z by Def4;

now :: thesis: for k being Element of NAT holds
( f2 . (k + 1) in SUCC ((f2 . k),(STC N)) & ( for j being Element of NAT st f2 . j in SUCC ((f2 . k),(STC N)) holds
k <= j ) )

let k be Element of NAT ; :: thesis: ( f2 . (k + 1) in SUCC ((f2 . k),(STC N)) & ( for j being Element of NAT st f2 . j in SUCC ((f2 . k),(STC N)) holds
k <= j ) )
reconsider fk = f2 . k as Element of NAT ;
A3: SUCC (fk,(STC N)) = {k,(k + 1)} by AMISTD_1:8;
thus f2 . (k + 1) in SUCC ((f2 . k),(STC N)) by A3, TARSKI:def 2; :: thesis: for j being Element of NAT st f2 . j in SUCC ((f2 . k),(STC N)) holds
k <= j
let j be Element of NAT ; :: thesis: ( f2 . j in SUCC ((f2 . k),(STC N)) implies k <= j )
assume f2 . j in SUCC ((f2 . k),(STC N)) ; :: thesis: k <= j
then ( j = k or j = k + 1 ) by A3, TARSKI:def 2;
hence k <= j by NAT_1:11; :: thesis: verum

end;

then for m, n being Element of NAT holds
( m <= n iff f2 . m <= f2 . n, STC N ) by Th3;
then ( z is Element of NAT & f = f2 ) by A1, Th2, ORDINAL1:def 12;
hence il. ((STC N),z) = z by A2; :: thesis: verum