let a, b be non zero Real; :: thesis: ( a + b = a * b iff (1 / a) + (1 / b) = 1 )
( (1 * a) / (a * b) = 1 / b & (1 * b) / (a * b) = 1 / a ) by XCMPLX_1:91;
then ((1 / a) + (1 / b)) * (a * b) = ((a + b) / (a * b)) * (a * b)
.= a + b by XCMPLX_1:87 ;
hence ( a + b = a * b iff (1 / a) + (1 / b) = 1 ) by XCMPLX_1:7; :: thesis: verum