let z, z1, z2 be Element of ; :: thesis: ( z <> 0. F_Complex implies (z1 / z) - (z2 / z) = (z1 - z2) / z )
reconsider z' = z, z1' = z1, z2' = z2 as Element of COMPLEX by Def1;
A1: z1' - z2' = z1 - z2 by Th5;
assume A2: z <> 0. F_Complex ; :: thesis: (z1 / z) - (z2 / z) = (z1 - z2) / z
then ( z1' / z' = z1 / z & z2' / z' = z2 / z ) by Th8;
hence (z1 / z) - (z2 / z) = (z1' / z') - (z2' / z') by Th5
.= (z1' - z2') / z' by XCMPLX_1:121
.= (z1 - z2) / z by A2, A1, Th8 ;
:: thesis: verum