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