let a, b, c be Complex; :: thesis: ( c <> 0 & a * c = b * c implies a = b )
assume A1: c <> 0 ; :: thesis: ( not a * c = b * c or a = b )
assume a * c = b * c ; :: thesis: a = b
then a * (c * (c ")) = (b * c) * (c ") by Th4;
then a * 1 = (b * c) * (c ") by A1, XCMPLX_0:def 7;
then a = b * (c * (c ")) ;
then a = b * 1 by A1, XCMPLX_0:def 7;
hence a = b ; :: thesis: verum