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