thus Im (1_ F_Complex ) = 0 by COMPLEX1:15, COMPLFLD:10; :: thesis: ( Im (- (1_ F_Complex )) = 0 & Im (0. F_Complex ) = 0 )
- (1_ F_Complex ) = - 1r by COMPLFLD:4, COMPLFLD:10;
hence Im (- (1_ F_Complex )) = - 0 by COMPLEX1:15, COMPLEX1:34
.= 0 ;
:: thesis: Im (0. F_Complex ) = 0
thus Im (0. F_Complex ) = 0 by COMPLEX1:12, COMPLFLD:9; :: thesis: verum