theorem Th9: :: TOPGEN_5:9

for a, b being Real holds |.|[a,b]|.| ^2 = (a ^2) + (b ^2)