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