let z, z1, z2 be Element of F_Complex; :: thesis: ( z <> 0. F_Complex implies (z1 / z) - (z2 / z) = (z1 - z2) / z )
reconsider z9 = z, z19 = z1, z29 = z2 as Element of COMPLEX by Def1;
A1: z19 - z29 = z1 - z2 by Th3;
assume A2: z <> 0. F_Complex ; :: thesis: (z1 / z) - (z2 / z) = (z1 - z2) / z
then ( z19 / z9 = z1 / z & z29 / z9 = z2 / z ) by Th6;
hence (z1 / z) - (z2 / z) = (z19 / z9) - (z29 / z9) by Th3
.= (z19 - z29) / z9 by XCMPLX_1:120
.= (z1 - z2) / z by A2, A1, Th6 ;
:: thesis: verum