let a be Ordinal; :: thesis: for f being Ordinal-Sequence st 0 in a & ( for b being Ordinal st b in dom f holds
f . b = a |^|^ b ) holds
f is non-decreasing
let f be Ordinal-Sequence; :: thesis: ( 0 in a & ( for b being Ordinal st b in dom f holds
f . b = a |^|^ b ) implies f is non-decreasing )
assume that
A1: 0 in a and
A2: for b being Ordinal st b in dom f holds
f . b = a |^|^ b ; :: thesis: f is non-decreasing
let b be Ordinal; :: according to ORDINAL5:def 2 :: thesis: for b being Ordinal st b in b & b in dom f holds
f . b c= f . b
let c be Ordinal; :: thesis: ( b in c & c in dom f implies f . b c= f . c )
assume A3: ( b in c & c in dom f ) ; :: thesis: f . b c= f . c
then b c= c by ORDINAL1:def 2;
then ( a |^|^ b c= a |^|^ c & a |^|^ c = f . c ) by A1, A2, A3, Th21;
hence f . b c= f . c by A2, A3, ORDINAL1:10; :: thesis: verum