theorem Th47: :: AFINSQ_2:48

for F being XFinSequence st F is real-valued holds
Sum F = addreal "**" F