let r1, r2, r3 be Real; :: thesis: Sum (sqr <*r1,r2,r3*>) = ((r1 ^2) + (r2 ^2)) + (r3 ^2)
thus Sum (sqr <*r1,r2,r3*>) = Sum <*(r1 ^2),(r2 ^2),(r3 ^2)*> by Th15
.= ((r1 ^2) + (r2 ^2)) + (r3 ^2) by RVSUM_1:78 ; :: thesis: verum