reconsider A = {} as finite Ordinal-Sequence ;
consider f being Ordinal-Sequence such that
A1:
Sum^ A = last f
and
A2:
dom f = succ (dom A)
and
A3:
f . 0 = 0
and
for n being Nat st n in dom A holds
f . (n + 1) = (f . n) +^ (A . n)
by Def8;
( dom f = succ 0 implies last f = f . 0 )
by ORDINAL2:6;
hence
Sum^ {} = 0
by A1, A2, A3; verum