let z2, z3, z1 be Element of F_Complex ; :: thesis: ( z2 <> 0. F_Complex & z3 <> 0. F_Complex implies (z1 * z3) / z2 = z1 / (z2 / z3) )
reconsider z1' = z1, z2' = z2, z3' = 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 = z2' / z3' by Th8;
A4: z2 / z3 <> 0. F_Complex by A1, A2, Th62;
thus (z1 * z3) / z2 = (z1' * z3') / z2' by A1, Th8
.= z1' / (z2' / z3') by XCMPLX_1:78
.= z1 / (z2 / z3) by A3, A4, Th8 ; :: thesis: verum