let a, b be complex number ; :: thesis: (a " ) * (b " ) = (a * b) "

per cases ( a = 0 or b = 0 or ( a <> 0 & b <> 0 ) ) ;

suppose A1: ( a = 0 or b = 0 ) ; :: thesis: (a " ) * (b " ) = (a * b) "

then ( a " = 0 or b " = 0 ) ;
hence (a " ) * (b " ) = (a * b) " by A1; :: thesis: verum

end;

suppose that A2: a <> 0 and
A3: b <> 0 ; :: thesis: (a " ) * (b " ) = (a * b) "

thus (a " ) * (b " ) = ((a " ) * (b " )) * 1
.= ((a " ) * (b " )) * ((a * b) * ((a * b) " )) by A2, A3, XCMPLX_0:def 7
.= (((a " ) * a) * ((b " ) * b)) * ((a * b) " )
.= (1 * ((b " ) * b)) * ((a * b) " ) by A2, XCMPLX_0:def 7
.= 1 * ((a * b) " ) by A3, XCMPLX_0:def 7
.= (a * b) " ; :: thesis: verum

end;

end;