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