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 16 :: thesis: phi | A is increasing
let B be Ordinal; :: according to ORDINAL2:def 16 :: 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 A2: ( B in C & C in dom (phi | A) ) ; :: thesis: (phi | A) . B in (phi | A) . C
dom (phi | A) c= dom phi by RELAT_1:89;
then ( B in dom (phi | A) & C in dom phi ) by A2, ORDINAL1:19;
then ( phi . B in phi . C & phi . B = (phi | A) . B & phi . C = (phi | A) . C ) by A1, A2, FUNCT_1:70;
hence (phi | A) . B in (phi | A) . C ; :: thesis: verum