let a, b be complex number ; :: thesis: ( a <> 0 & b <> 0 implies (a " ) + (b " ) = (a + b) * ((a * b) " ) )
assume that
A1: a <> 0 and
A2: b <> 0 ; :: thesis: (a " ) + (b " ) = (a + b) * ((a * b) " )
b " = (b " ) * 1 ;
then b " = (b " ) * ((a " ) * a) by A1, XCMPLX_0:def 7;
then b " = ((a " ) * (b " )) * a ;
then A3: b " = ((a * b) " ) * a by Lm1;
a " = (a " ) * 1 ;
then a " = (a " ) * ((b " ) * b) by A2, XCMPLX_0:def 7;
then a " = ((a " ) * (b " )) * b ;
then a " = ((a * b) " ) * b by Lm1;
hence (a " ) + (b " ) = (a + b) * ((a * b) " ) by A3; :: thesis: verum