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;
end;
end;
hence fi . A c= fi . B ; :: thesis: verum