let a, b be Element of F_Complex; :: thesis: ( Im a = 0 implies ( Re (a * b) = (Re a) * (Re b) & Im (a * b) = (Re a) * (Im b) ) )
assume A1: Im a = 0 ; :: thesis: ( Re (a * b) = (Re a) * (Re b) & Im (a * b) = (Re a) * (Im b) )
hence Re (a * b) = ((Re a) * (Re b)) - (0 * (Im b)) by HAHNBAN1:11
.= (Re a) * (Re b) ;
:: thesis: Im (a * b) = (Re a) * (Im b)
thus Im (a * b) = ((Re a) * (Im b)) + ((Re b) * 0) by A1, HAHNBAN1:11
.= (Re a) * (Im b) ; :: thesis: verum