theorem Th26: :: ORDINAL7:13

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