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