for p being FinSequence of F_Real
for q being real-valued FinSequence st p = q holds
Sum p = Sum q