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:32
.= addcomplex . ((a *'),b) by BINOP_2:def 3 ;
hence (addcomplex . (a,(b *'))) *' = addcomplex . ((a *'),b) ; :: thesis: verum