theorem Th15: :: BORSUK_7:16

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