theorem :: RVSUM_1:55

for r being Real holds sqr <*r*> = <*(r ^2)*>