theorem Th1: :: COMPLEX1:1

for a, b being Real st (a ^2) + (b ^2) = 0 holds
a = 0