ex f being Ordinal-Sequence st
( Sum^ {} = last f & dom f = succ (dom {}) & f . 0 = 0 & ( for n being Nat st n in dom {} holds
f . (n + 1) = (f . n) +^ ({} . n) ) ) by SUM;
hence Sum^ {} = 0 by ORDINAL2:7; :: thesis: verum