let c, a, b be complex number ; :: 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