let a be Ordinal; :: thesis: for f being Ordinal-Sequence st 1 in a & ( for b being Ordinal st b in dom f holds
f . b = exp (a,b) ) holds
f is increasing
let f be Ordinal-Sequence; :: thesis: ( 1 in a & ( for b being Ordinal st b in dom f holds
f . b = exp (a,b) ) implies f is increasing )
assume A1: ( 1 in a & ( for b being Ordinal st b in dom f holds
f . b = exp (a,b) ) ) ; :: thesis: f is increasing
let b be Ordinal; :: according to ORDINAL2:def 12 :: thesis: for b₁ being set holds
( not b in b₁ or not b₁ in dom f or f . b in f . b₁ )
let d be Ordinal; :: thesis: ( not b in d or not d in dom f or f . b in f . d )
assume A2: ( b in d & d in dom f ) ; :: thesis: f . b in f . d
then ( f . b = exp (a,b) & f . d = exp (a,d) ) by A1, ORDINAL1:10;
hence f . b in f . d by A1, A2, ORDINAL4:24; :: thesis: verum