let z1, z2 be Element of COMPLEX ; :: thesis: ( Im z1 = 0 & Im z2 = 0 & Re z2 <> 0 implies ( Re (z1 / z2) = (Re z1) / (Re z2) & Im (z1 / z2) = 0 ) )
assume A1: ( Im z1 = 0 & Im z2 = 0 & Re z2 <> 0 ) ; :: thesis: ( Re (z1 / z2) = (Re z1) / (Re z2) & Im (z1 / z2) = 0 )
then A2: ( z1 / z2 = z1 * (z2 " ) & Im (z2 " ) = 0 ) by Th79, XCMPLX_0:def 9;
hence Re (z1 / z2) = (Re z1) * (Re (z2 " )) by A1, Th30
.= (Re z1) * ((Re z2) " ) by A1, Th79
.= (Re z1) / (Re z2) by XCMPLX_0:def 9 ;
:: thesis: Im (z1 / z2) = 0
thus Im (z1 / z2) = 0 by A1, A2, Th30; :: thesis: verum