let f be Ordinal-Sequence; :: thesis: ( f = id a implies f is increasing )
assume A1: f = id a ; :: 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 A2: ( b in c & c in dom f ) ; :: thesis: f . b in f . c
then ( b in dom f & dom f = a ) by A1, ORDINAL1:10;
then ( f . b = b & f . c = c ) by A1, A2, FUNCT_1:18;
hence f . b in f . c by A2; :: thesis: verum