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