let f be Ordinal-Sequence; ( f is decreasing implies f is non-increasing )
assume A2:
for a, b being ordinal number st a in b & b in dom f holds
f . b in f . a
; ORDINAL5:def 1 f is non-increasing
let a be ordinal number ; ORDINAL5:def 3 for b being ordinal number st a in b & b in dom f holds
f . b c= f . a
let b be ordinal number ; ( a in b & b in dom f implies f . b c= f . a )
( f . b in f . a implies f . b c= f . a )
by ORDINAL1:def 2;
hence
( a in b & b in dom f implies f . b c= f . a )
by A2; verum