let fi be Ordinal-Sequence; :: thesis: for C being Ordinal st 1 in C & ( for A being Ordinal st A in dom fi holds

fi . A = exp (C,A) ) holds

fi is increasing

let C be Ordinal; :: thesis: ( 1 in C & ( for A being Ordinal st A in dom fi holds

fi . A = exp (C,A) ) implies fi is increasing )

assume that

A1: 1 in C and

A2: for A being Ordinal st A in dom fi holds

fi . A = exp (C,A) ; :: thesis: fi 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 fi or fi . A in fi . b_{1} )

let B be Ordinal; :: thesis: ( not A in B or not B in dom fi or fi . A in fi . B )

assume that

A3: A in B and

A4: B in dom fi ; :: thesis: fi . A in fi . B

A5: fi . B = exp (C,B) by A2, A4;

fi . A = exp (C,A) by A2, A3, A4, ORDINAL1:10;

hence fi . A in fi . B by A1, A3, A5, Th24; :: thesis: verum

fi . A = exp (C,A) ) holds

fi is increasing

let C be Ordinal; :: thesis: ( 1 in C & ( for A being Ordinal st A in dom fi holds

fi . A = exp (C,A) ) implies fi is increasing )

assume that

A1: 1 in C and

A2: for A being Ordinal st A in dom fi holds

fi . A = exp (C,A) ; :: thesis: fi 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 fi or fi . A in fi . B )

assume that

A3: A in B and

A4: B in dom fi ; :: thesis: fi . A in fi . B

A5: fi . B = exp (C,B) by A2, A4;

fi . A = exp (C,A) by A2, A3, A4, ORDINAL1:10;

hence fi . A in fi . B by A1, A3, A5, Th24; :: thesis: verum