:: deftheorem defines sqr RVSUM_1:def 8 :
for F being real-valued FinSequence holds sqr F = sqrreal * F;