let fi be Ordinal-Sequence; :: thesis: for A being Ordinal st fi is increasing & A in dom fi holds

A c= fi . A

let A be Ordinal; :: thesis: ( fi is increasing & A in dom fi implies A c= fi . A )

assume that

A1: for A, B being Ordinal st A in B & B in dom fi holds

fi . A in fi . B and

A2: A in dom fi and

A3: not A c= fi . A ; :: according to ORDINAL2:def 12 :: thesis: contradiction

defpred S_{1}[ set ] means ( $1 in dom fi & not $1 c= fi . $1 );

A4: ex A being Ordinal st S_{1}[A]
by A2, A3;

consider A being Ordinal such that

A5: S_{1}[A]
and

A6: for B being Ordinal st S_{1}[B] holds

A c= B from ORDINAL1:sch 1(A4);

reconsider B = fi . A as Ordinal ;

A7: B in A by A5, ORDINAL1:16;

then not B c= fi . B by A1, A5, ORDINAL1:5;

hence contradiction by A5, A6, A7, ORDINAL1:10; :: thesis: verum

A c= fi . A

let A be Ordinal; :: thesis: ( fi is increasing & A in dom fi implies A c= fi . A )

assume that

A1: for A, B being Ordinal st A in B & B in dom fi holds

fi . A in fi . B and

A2: A in dom fi and

A3: not A c= fi . A ; :: according to ORDINAL2:def 12 :: thesis: contradiction

defpred S

A4: ex A being Ordinal st S

consider A being Ordinal such that

A5: S

A6: for B being Ordinal st S

A c= B from ORDINAL1:sch 1(A4);

reconsider B = fi . A as Ordinal ;

A7: B in A by A5, ORDINAL1:16;

then not B c= fi . B by A1, A5, ORDINAL1:5;

hence contradiction by A5, A6, A7, ORDINAL1:10; :: thesis: verum