theorem Th16: :: BORSUK_7:17

for r1, r2, r3 being Real holds Sum (sqr <*r1,r2,r3*>) = ((r1 ^2) + (r2 ^2)) + (r3 ^2)