let fi be Ordinal-Sequence; :: thesis: for C being Ordinal st C <> {} & ( for A being Ordinal st A in dom fi holds
fi . A = A *^ C ) holds
fi is increasing
let C be Ordinal; :: thesis: ( C <> {} & ( for A being Ordinal st A in dom fi holds
fi . A = A *^ C ) implies fi is increasing )
assume that
A1: C <> {} and
A2: for A being Ordinal st A in dom fi holds
fi . A = A *^ C ; :: thesis: fi is increasing
let A be Ordinal; :: according to ORDINAL2:def 12 :: 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 that
A3: A in B and
A4: B in dom fi ; :: thesis: fi . A in fi . B
A5: fi . B = B *^ C by A2, A4;
fi . A = A *^ C by A2, A3, A4, ORDINAL1:10;
hence fi . A in fi . B by A1, A3, A5, ORDINAL2:40; :: thesis: verum