let a be Ordinal; :: thesis: for f being Ordinal-Sequence st f is non-decreasing holds
f | a is non-decreasing
let f be Ordinal-Sequence; :: thesis: ( f is non-decreasing implies f | a is non-decreasing )
assume A1: for b, c being Ordinal st b in c & c in dom f holds
f . b c= f . c ; :: according to ORDINAL5:def 2 :: thesis: f | a is non-decreasing
let b be Ordinal; :: according to ORDINAL5:def 2 :: thesis: for b₁ being set holds
( not b in b₁ or not b₁ in dom (f | a) or (f | a) . b c= (f | a) . b₁ )
let c be Ordinal; :: thesis: ( not b in c or not c in dom (f | a) or (f | a) . b c= (f | a) . c )
assume A2: ( b in c & c in dom (f | a) ) ; :: thesis: (f | a) . b c= (f | a) . c
then A3: ( c in dom f & c in a ) by RELAT_1:57;
then ( (f | a) . b = f . b & (f | a) . c = f . c ) by A2, FUNCT_1:49, ORDINAL1:10;
hence (f | a) . b c= (f | a) . c by A1, A2, A3; :: thesis: verum