theorem :: RVSUM_1:70

for F1, F2 being real-valued FinSequence holds sqr (mlt (F1,F2)) = mlt ((sqr F1),(sqr F2))