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_{1} being set holds

( not B in b_{1} or not b_{1} in dom (phi | A) or (phi | A) . B in (phi | A) . b_{1} )

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

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

( not B in 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