for a being Ordinal
for n being Nat holds Sum^ (n --> a) = n *^ a