- 1r = - (1_ F_Complex) by COMPLFLD:4, COMPLFLD:10;
hence (- (1_ F_Complex)) * (- (1_ F_Complex)) = 1_ F_Complex by COMPLFLD:10; :: thesis: verum