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