let z1, z2, z3 be Element of F_Complex; :: thesis: ( z2 <> 0. F_Complex & z3 <> 0. F_Complex implies (z1 * z3) / z2 = z1 / (z2 / z3) )
reconsider z19 = z1, z29 = z2, z39 = z3 as Element of COMPLEX by Def1;
assume A1: z2 <> 0. F_Complex ; :: thesis: ( not z3 <> 0. F_Complex or (z1 * z3) / z2 = z1 / (z2 / z3) )
assume A2: z3 <> 0. F_Complex ; :: thesis: (z1 * z3) / z2 = z1 / (z2 / z3)
then A3: z2 / z3 <> 0. F_Complex by A1, Th26;
A4: z2 / z3 = z29 / z39 by A2, Th6;
thus (z1 * z3) / z2 = (z19 * z39) / z29 by A1, Th6
.= z19 / (z29 / z39) by XCMPLX_1:77
.= z1 / (z2 / z3) by A4, A3, Th6 ; :: thesis: verum