let z2, z1, 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 z2' = 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 ) )
assume A2:
( z1 * z2 = z3 or z2 * z1 = z3 )
; :: thesis: ( z1 = z3 * (z2 " ) & z1 = (z2 " ) * z3 )
A3:
z2 " = z2' "
by A1, Th7;