let z, z1, z2 be Element of F_Complex ; :: 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;
assume A1: z <> 0. F_Complex ; :: thesis: (z1 / z) - (z2 / z) = (z1 - z2) / z
A2: z1' - z2' = z1 - z2 by Th5;
( z1' / z' = z1 / z & z2' / z' = z2 / z ) by A1, Th8;
hence (z1 / z) - (z2 / z) = (z1' / z') - (z2' / z') by Th5
.= (z1' - z2') / z' by XCMPLX_1:121
.= (z1 - z2) / z by A1, A2, Th8 ;
:: thesis: verum