theorem Th4: :: HAHNBAN1:5
(- (1_ F_Complex)) * (- (1_ F_Complex)) = 1_ F_Complex