let C be Ordinal; :: thesis: for phi being Ordinal-Sequence st phi is increasing holds

C +^ phi is increasing

let phi be Ordinal-Sequence; :: thesis: ( phi is increasing implies C +^ phi is increasing )

assume A1: phi is increasing ; :: thesis: C +^ phi is increasing

let A be Ordinal; :: according to ORDINAL2:def 12 :: thesis: for b_{1} being set holds

( not A in b_{1} or not b_{1} in dom (C +^ phi) or (C +^ phi) . A in (C +^ phi) . b_{1} )

let B be Ordinal; :: thesis: ( not A in B or not B in dom (C +^ phi) or (C +^ phi) . A in (C +^ phi) . B )

set xi = C +^ phi;

assume that

A2: A in B and

A3: B in dom (C +^ phi) ; :: thesis: (C +^ phi) . A in (C +^ phi) . B

reconsider A9 = phi . A, B9 = phi . B as Ordinal ;

A4: dom (C +^ phi) = dom phi by ORDINAL3:def 1;

then A5: (C +^ phi) . B = C +^ B9 by A3, ORDINAL3:def 1;

A in dom (C +^ phi) by A2, A3, ORDINAL1:10;

then A6: (C +^ phi) . A = C +^ A9 by A4, ORDINAL3:def 1;

A9 in B9 by A1, A2, A3, A4;

hence (C +^ phi) . A in (C +^ phi) . B by A6, A5, ORDINAL2:32; :: thesis: verum

C +^ phi is increasing

let phi be Ordinal-Sequence; :: thesis: ( phi is increasing implies C +^ phi is increasing )

assume A1: phi is increasing ; :: thesis: C +^ phi is increasing

let A be Ordinal; :: according to ORDINAL2:def 12 :: thesis: for b

( not A in b

let B be Ordinal; :: thesis: ( not A in B or not B in dom (C +^ phi) or (C +^ phi) . A in (C +^ phi) . B )

set xi = C +^ phi;

assume that

A2: A in B and

A3: B in dom (C +^ phi) ; :: thesis: (C +^ phi) . A in (C +^ phi) . B

reconsider A9 = phi . A, B9 = phi . B as Ordinal ;

A4: dom (C +^ phi) = dom phi by ORDINAL3:def 1;

then A5: (C +^ phi) . B = C +^ B9 by A3, ORDINAL3:def 1;

A in dom (C +^ phi) by A2, A3, ORDINAL1:10;

then A6: (C +^ phi) . A = C +^ A9 by A4, ORDINAL3:def 1;

A9 in B9 by A1, A2, A3, A4;

hence (C +^ phi) . A in (C +^ phi) . B by A6, A5, ORDINAL2:32; :: thesis: verum