let a, b be Element of COMPLEX ; :: thesis: (addcomplex . a,(b *' )) *' = addcomplex . (a *' ),b
(addcomplex . a,(b *' )) *' = (a + (b *' )) *' by BINOP_2:def 3
.= (a *' ) + ((b *' ) *' ) by COMPLEX1:118
.= addcomplex . (a *' ),b by BINOP_2:def 3 ;
hence (addcomplex . a,(b *' )) *' = addcomplex . (a *' ),b ; :: thesis: verum