let fi be Ordinal-Sequence; :: thesis: for A, B being Ordinal st fi is increasing & A c= B & B in dom fi holds
fi . A c= fi . B
let A, B be Ordinal; :: thesis: ( fi is increasing & A c= B & B in dom fi implies fi . A c= fi . B )
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 c= B and
A3: B in dom fi ; :: according to ORDINAL2:def 12 :: thesis: fi . A c= fi . B
reconsider C = fi . B as Ordinal ;

now :: thesis: fi . A c= fi . B

per cases ( A = B or A <> B ) ;

suppose A = B ; :: thesis: fi . A c= fi . B

hence fi . A c= fi . B ; :: thesis: verum

end;

suppose A <> B ; :: thesis: fi . A c= fi . B

then A c< B by A2;
then A in B by ORDINAL1:11;
then fi . A in C by A1, A3;
hence fi . A c= fi . B by ORDINAL1:def 2; :: thesis: verum

end;

end;

end;

hence fi . A c= fi . B ; :: thesis: verum