theorem Th75: :: COMPLEX1:75

for a being Real holds |.a.| ^2 = a ^2