reconsider f = id NAT as sequence of NAT ;
set M = STC N;
now 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 ;
( 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;
for j being Element of NAT st f . j in SUCC ((f . k),(STC N)) holds
k <= jlet j be
Element of
NAT ;
( f . j in SUCC ((f . k),(STC N)) implies k <= j )assume
f . j in SUCC (
(f . k),
(STC N))
;
k <= jthen
(
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;
verum end;
hence
STC N is weakly_standard
by Th4; verum