reconsider f = id NAT as sequence of NAT ;
set M = STC N;

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

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

end;

hence STC N is weakly_standard by Th4; :: thesis: verum