:: deftheorem Def15 defines *^ ORDINAL2:def 15 :
for A, B, b₃ being Ordinal holds
( b₃ = A *^ B iff ex fi being Ordinal-Sequence st
( b₃ = last fi & dom fi = succ A & fi . 0 = 0 & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = (fi . C) +^ B ) & ( for C being Ordinal st C in succ A & C <> 0 & C is limit_ordinal holds
fi . C = union (sup (fi | C)) ) ) );