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