let phi be Ordinal-Sequence; :: thesis: for A being Ordinal st phi is increasing holds
phi | A is increasing
let A be Ordinal; :: thesis: ( phi is increasing implies phi | A is increasing )
assume A1: for A, B being Ordinal st A in B & B in dom phi holds
phi . A in phi . B ; :: according to ORDINAL2:def 12 :: thesis: phi | A 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 (phi | A) or (phi | A) . B in (phi | A) . b₁ )
let C be Ordinal; :: thesis: ( not B in C or not C in dom (phi | A) or (phi | A) . B in (phi | A) . C )
assume that
A2: B in C and
A3: C in dom (phi | A) ; :: thesis: (phi | A) . B in (phi | A) . C
A4: phi . B = (phi | A) . B by A2, A3, FUNCT_1:47, ORDINAL1:10;
dom (phi | A) c= dom phi by RELAT_1:60;
then phi . B in phi . C by A1, A2, A3;
hence (phi | A) . B in (phi | A) . C by A3, A4, FUNCT_1:47; :: thesis: verum