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 ") & z1 = (z2 ") * z3 ) )
reconsider 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 ") & z1 = (z2 ") * z3 ) )
then A2: z2 " = z29 " by Th5;
assume A3: ( z1 * z2 = z3 or z2 * z1 = z3 ) ; :: thesis: ( z1 = z3 * (z2 ") & z1 = (z2 ") * z3 )

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

suppose z1 * z2 = z3 ; :: thesis: ( z1 = z3 * (z2 ") & z1 = (z2 ") * z3 )

hence ( z1 = z3 * (z2 ") & z1 = (z2 ") * z3 ) by A1, A2, Th7, XCMPLX_1:203; :: thesis: verum

end;

suppose z2 * z1 = z3 ; :: thesis: ( z1 = z3 * (z2 ") & z1 = (z2 ") * z3 )

hence ( z1 = z3 * (z2 ") & z1 = (z2 ") * z3 ) by A1, A2, Th7, XCMPLX_1:203; :: thesis: verum

end;

end;