:: deftheorem Def8 defines Sum^ ORDINAL5:def 8 :
for A being finite Ordinal-Sequence
for b₂ being Ordinal holds
( b₂ = Sum^ A iff ex f being Ordinal-Sequence st
( b₂ = last f & dom f = succ (dom A) & f . 0 = 0 & ( for n being Nat st n in dom A holds
f . (n + 1) = (f . n) +^ (A . n) ) ) );