theorem Th4: :: HAHNBAN1:5

(- (1_ F_Complex)) * (- (1_ F_Complex)) = 1_ F_Complex