let p, q, s, t be Real; :: thesis: ( p * s < 0 & p > 0 implies ( ((t - q) / (p - s)) + (t / s) = (1 / s) * (((t * p) - (q * s)) / (p - s)) & ((t - q) / (p - s)) + (q / p) = (1 / p) * (((t * p) - (q * s)) / (p - s)) ) )
assume A2: ( p * s < 0 & p > 0 ) ; :: thesis: ( ((t - q) / (p - s)) + (t / s) = (1 / s) * (((t * p) - (q * s)) / (p - s)) & ((t - q) / (p - s)) + (q / p) = (1 / p) * (((t * p) - (q * s)) / (p - s)) )
then A7: p - s <> 0 ;
s < 0 by A2;
then PS: ((t - q) / (p - s)) + (t / s) = (((t - q) * s) + (t * (p - s))) / ((p - s) * s) by XCMPLX_1:116, A2
.= (1 / s) * (((t * p) - (q * s)) / (p - s)) by XCMPLX_1:103 ;
((t - q) / (p - s)) + (q / p) = (((t - q) * p) + (q * (p - s))) / ((p - s) * p) by XCMPLX_1:116, A7, A2
.= ((t * p) - (q * s)) / ((p - s) * p) ;
hence ( ((t - q) / (p - s)) + (t / s) = (1 / s) * (((t * p) - (q * s)) / (p - s)) & ((t - q) / (p - s)) + (q / p) = (1 / p) * (((t * p) - (q * s)) / (p - s)) ) by XCMPLX_1:103, PS; :: thesis: verum