let a, b be Complex; :: 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;