let a be Ordinal; Sum^ <%a%> = a
consider f being Ordinal-Sequence such that
A1:
( Sum^ <%a%> = 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) ) )
by Def8;
A2:
( dom <%a%> = 1 & <%a%> . 0 = a )
by AFINSQ_1:def 4;
0 in Segm 1
by NAT_1:44;
then f . (0 + 1) =
0 +^ a
by A1, A2
.=
a
by ORDINAL2:30
;
hence
Sum^ <%a%> = a
by A1, A2, ORDINAL2:6; verum