theorem :: RVSUM_1:56

for i being natural Number
for r being Real holds sqr (i |-> r) = i |-> (r ^2)