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 Th11
.= 0 ;
:: thesis: verum