theorem Th50: :: AFINSQ_2:51

for F being XFinSequence st F is natural-valued holds
Sum F = addnat "**" F