let fi be Ordinal-Sequence; :: thesis: for C being Ordinal st {} <> dom fi & C <> {} & sup fi is limit_ordinal holds
sup (fi *^ C) = (sup fi) *^ C
let C be Ordinal; :: thesis: ( {} <> dom fi & C <> {} & sup fi is limit_ordinal implies sup (fi *^ C) = (sup fi) *^ C )
A1: for A, B being Ordinal st A in dom fi & B = fi . A holds
(fi *^ C) . A = B *^ C by Def4;
dom (fi *^ C) = dom fi by Def4;
hence ( {} <> dom fi & C <> {} & sup fi is limit_ordinal implies sup (fi *^ C) = (sup fi) *^ C ) by A1, Th42; :: thesis: verum