let m be Complex; :: thesis: for x, y, z being non zero Complex holds
( ((x / y) + (y / z)) + (z / x) = m iff (((x ^2) * z) + ((y ^2) * x)) + ((z ^2) * y) = ((m * x) * y) * z )
let x, y, z be non zero Complex; :: thesis: ( ((x / y) + (y / z)) + (z / x) = m iff (((x ^2) * z) + ((y ^2) * x)) + ((z ^2) * y) = ((m * x) * y) * z )
(x / y) + (y / z) = ((x * z) + (y * y)) / (y * z) by XCMPLX_1:116;
then A1: ((x / y) + (y / z)) + (z / x) = ((((x * z) + (y * y)) * x) + ((z * y) * z)) / ((y * z) * x) by XCMPLX_1:116;
thus ( ((x / y) + (y / z)) + (z / x) = m implies (((x ^2) * z) + ((y ^2) * x)) + ((z ^2) * y) = ((m * x) * y) * z ) :: thesis: ( (((x ^2) * z) + ((y ^2) * x)) + ((z ^2) * y) = ((m * x) * y) * z implies ((x / y) + (y / z)) + (z / x) = m )

proof

assume ((x / y) + (y / z)) + (z / x) = m ; :: thesis: (((x ^2) * z) + ((y ^2) * x)) + ((z ^2) * y) = ((m * x) * y) * z
then (((((x * z) + (y * y)) * x) + ((z * y) * z)) / ((x * y) * z)) * ((x * y) * z) = m * ((x * y) * z) by A1;
hence (((x ^2) * z) + ((y ^2) * x)) + ((z ^2) * y) = ((m * x) * y) * z by XCMPLX_1:87; :: thesis: verum

end;

assume (((x ^2) * z) + ((y ^2) * x)) + ((z ^2) * y) = ((m * x) * y) * z ; :: thesis: ((x / y) + (y / z)) + (z / x) = m
then ((((x ^2) * z) + ((y ^2) * x)) + ((z ^2) * y)) / ((x * y) * z) = (m * ((x * y) * z)) / ((x * y) * z) ;
hence ((x / y) + (y / z)) + (z / x) = m by A1, XCMPLX_1:89; :: thesis: verum