theorem :: RVSUM_1:144

for f, g being real-valued FinSequence holds sqr (f ^ g) = (sqr f) ^ (sqr g)