let a, b be Element of F_Complex; :: thesis: ( Im a = 0 & Im b = 0 implies Im (a * b) = 0 )
assume ( Im a = 0 & Im b = 0 ) ; :: thesis: Im (a * b) = 0
hence Im (a * b) = (Re b) * 0 by Th10
.= 0 ;
:: thesis: verum