theorem Th10: :: TOPREAL6:11

for a, b being Real holds sqr <*a,b*> = <*(a ^2),(b ^2)*>