let a be Ordinal; :: thesis: for n being Nat holds Sum^ (n --> a) = n *^ a
let n be Nat; :: thesis: Sum^ (n --> a) = n *^ a
consider fi being Ordinal-Sequence such that
A1: ( Sum^ (n --> a) = last fi & dom fi = succ (dom (n --> a)) & fi . 0 = 0 ) and
A2: for k being Nat st k in dom (n --> a) holds
fi . (k + 1) = (fi . k) +^ ((n --> a) . k) by ORDINAL5:def 8;

A4: now :: thesis: for C being Ordinal st succ C in succ n holds
fi . (succ C) = (fi . C) +^ a

let C be Ordinal; :: thesis: ( succ C in succ n implies fi . (succ C) = (fi . C) +^ a )
assume succ C in succ n ; :: thesis: fi . (succ C) = (fi . C) +^ a
then A5: C in n by ORDINAL3:3;
n in omega by ORDINAL1:def 12;
then C in omega by A5, ORDINAL1:10;
then reconsider k = C as Nat ;
A6: k in dom (n --> a) by A5;
thus fi . (succ C) = fi . (succ (Segm C))
.= fi . (Segm (k + 1)) by NAT_1:38
.= (fi . k) +^ ((n --> a) . k) by A2, A6
.= (fi . C) +^ a by A5, FUNCOP_1:7 ; :: thesis: verum

end;

now :: thesis: for C being Ordinal st C in succ n & C <> 0 & C is limit_ordinal holds
fi . C = union (sup (fi | C))

let C be Ordinal; :: thesis: ( C in succ n & C <> 0 & C is limit_ordinal implies fi . C = union (sup (fi | C)) )
assume A7: ( C in succ n & C <> 0 & C is limit_ordinal ) ; :: thesis: fi . C = union (sup (fi | C))
succ n in omega by ORDINAL1:def 12;
then C in omega by A7, ORDINAL1:10;
hence fi . C = union (sup (fi | C)) by A7; :: thesis: verum

end;

hence Sum^ (n --> a) = n *^ a by A1, A4, ORDINAL2:def 15; :: thesis: verum