let z1, z2, z3 be Element of F_Complex; :: thesis: ( z2 <> 0. F_Complex & ( z1 * z2 = z3 or z2 * z1 = z3 ) implies z1 = z3 / z2 )
reconsider z39 = z3, z29 = z2 as Element of COMPLEX by Def1;
assume A1: z2 <> 0. F_Complex ; :: thesis: ( ( not z1 * z2 = z3 & not z2 * z1 = z3 ) or z1 = z3 / z2 )
assume A2: ( z1 * z2 = z3 or z2 * z1 = z3 ) ; :: thesis: z1 = z3 / z2

per cases ( z1 * z2 = z3 or z2 * z1 = z3 ) by A2;

suppose z1 * z2 = z3 ; :: thesis: z1 = z3 / z2

hence z1 = z39 / z29 by A1, Th7, XCMPLX_1:89
.= z3 / z2 by A1, Th6 ;
:: thesis: verum

end;

suppose z2 * z1 = z3 ; :: thesis: z1 = z3 / z2

hence z1 = z39 / z29 by A1, Th7, XCMPLX_1:89
.= z3 / z2 by A1, Th6 ;
:: thesis: verum

end;

end;