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 = exp (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 = exp (a,b) ) implies f is non-decreasing )
assume A1: ( 0 in a & ( for b being Ordinal st b in dom f holds
f . b = exp (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 d be Ordinal; :: thesis: ( b in d & d in dom f implies f . b c= f . d )
assume A2: ( b in d & d in dom f ) ; :: thesis: f . b c= f . d
then b in dom f by ORDINAL1:10;
then ( b c= d & f . b = exp (a,b) & f . d = exp (a,d) ) by A1, A2, ORDINAL1:def 2;
hence f . b c= f . d by A1, ORDINAL4:27; :: thesis: verum