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 & not A c= fi . A ) ; :: according to ORDINAL2:def 16 :: thesis: contradiction
defpred S₁[ set ] means ( $1 in dom fi & not $1 c= fi . $1 );
A3: ex A being Ordinal st S₁[A] by A2;
consider A being Ordinal such that
A4: S₁[A] and
A5: for B being Ordinal st S₁[B] holds
A c= B from ORDINAL1:sch 1(A3);
reconsider B = fi . A as Ordinal ;
A6: B in A by A4, ORDINAL1:26;
then fi . B in B by A1, A4;
then ( B in dom fi & not B c= fi . B ) by A4, A6, ORDINAL1:7, ORDINAL1:19;
hence contradiction by A4, A5; :: thesis: verum