let a be Ordinal; :: thesis: for f being Ordinal-Sequence st 1 in a & dom f c= omega & ( for b being Ordinal st b in dom f holds
f . b = a |^|^ b ) holds
f is increasing
let f be Ordinal-Sequence; :: thesis: ( 1 in a & dom f c= omega & ( for b being Ordinal st b in dom f holds
f . b = a |^|^ b ) implies f is increasing )
assume that
A1: 1 in a and
A2: dom f c= omega and
A3: for n being Ordinal st n in dom f holds
f . n = a |^|^ n ; :: 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 c be Ordinal; :: thesis: ( not b in c or not c in dom f or f . b in f . c )
assume A4: ( b in c & c in dom f ) ; :: thesis: f . b in f . c
then A5: b in dom f by ORDINAL1:10;
reconsider b = b, c = c as Element of omega by A2, A4, ORDINAL1:10;
b in Segm c by A4;
then ( f . b = a |^|^ b & f . c = a |^|^ c & b < c ) by A3, A4, A5, NAT_1:44;
hence f . b in f . c by A1, Th24; :: thesis: verum