for fi being Ordinal-Sequence
for C being Ordinal st {} <> dom fi & C <> {} & sup fi is limit_ordinal holds
sup (fi *^ C) = (sup fi) *^ C