let fi be Ordinal-Sequence; :: thesis: for C being Ordinal st ( for A being Ordinal st A in dom fi holds
fi . A = C +^ A ) holds
fi is increasing
let C be Ordinal; :: thesis: ( ( for A being Ordinal st A in dom fi holds
fi . A = C +^ A ) implies fi is increasing )
assume A1: for A being Ordinal st A in dom fi holds
fi . A = C +^ A ; :: thesis: fi is increasing
let A be Ordinal; :: according to ORDINAL2:def 16 :: thesis: for b₁ being set holds
( not A in b₁ or not b₁ in dom fi or fi . A in fi . b₁ )
let B be Ordinal; :: thesis: ( not A in B or not B in dom fi or fi . A in fi . B )
assume A2: ( A in B & B in dom fi ) ; :: thesis: fi . A in fi . B
then ( fi . A = C +^ A & fi . B = C +^ B ) by A1, ORDINAL1:19;
hence fi . A in fi . B by A2, ORDINAL2:49; :: thesis: verum