let x1 be Element of COMPLEX ; :: according to BINOP_1:def 20 :: thesis: for b₁ being Element of COMPLEX holds sqrcomplex . (multcomplex . x1,b₁) = multcomplex . (sqrcomplex . x1),(sqrcomplex . b₁)
let x2 be Element of COMPLEX ; :: thesis: sqrcomplex . (multcomplex . x1,x2) = multcomplex . (sqrcomplex . x1),(sqrcomplex . x2)
thus sqrcomplex . (multcomplex . x1,x2) = sqrcomplex . (x1 * x2) by BINOP_2:def 5
.= (x1 * x2) ^2 by Def2
.= (x1 ^2 ) * (x2 ^2 )
.= multcomplex . (x1 ^2 ),(x2 ^2 ) by BINOP_2:def 5
.= multcomplex . (sqrcomplex . x1),(x2 ^2 ) by Def2
.= multcomplex . (sqrcomplex . x1),(sqrcomplex . x2) by Def2 ; :: thesis: verum