let a be ordinal number ; :: thesis: for f being Ordinal-Sequence st 1 in a & dom f c= omega & ( for b being ordinal number 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 number st b in dom f holds
f . b = a |^|^ b ) implies f is increasing )
assume that
Z0: 1 in a and
Z1: dom f c= omega and
Z2: for n being Ordinal st n in dom f holds
f . n = a |^|^ n ; :: thesis: f is increasing
let b be ordinal number ; :: according to ORDINAL2:def 16 :: thesis: for b₁ being set holds
( not b in b₁ or not b₁ in proj1 f or f . b in f . b₁ )
let c be ordinal number ; :: thesis: ( not b in c or not c in proj1 f or f . b in f . c )
assume Z3: ( b in c & c in dom f ) ; :: thesis: f . b in f . c
then Z4: b in dom f by ORDINAL1:19;
then reconsider b = b, c = c as Element of omega by Z1, Z3;
( f . b = a |^|^ b & f . c = a |^|^ c & b < c ) by Z2, Z3, Z4, NAT_1:45;
hence f . b in f . c by Z0, Th7; :: thesis: verum