thus Im (1_ F_Complex) = 0 by COMPLEX1:6, COMPLFLD:8; :: thesis: ( Im (- (1_ F_Complex)) = 0 & Im (0. F_Complex) = 0 )
- (1_ F_Complex) = - 1r by COMPLFLD:2, COMPLFLD:8;
hence Im (- (1_ F_Complex)) = - 0 by COMPLEX1:6, COMPLEX1:17
.= 0 ;
:: thesis: Im (0. F_Complex) = 0
thus Im (0. F_Complex) = 0 by COMPLEX1:4, COMPLFLD:7; :: thesis: verum