theorem :: RVSUM_1:67

for F being real-valued FinSequence holds sqr F = mlt (F,F) ;