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 Def1
.= (x1 ^2) * (x2 ^2)
.= multcomplex . ((x1 ^2),(x2 ^2)) by BINOP_2:def 5
.= multcomplex . ((sqrcomplex . x1),(x2 ^2)) by Def1
.= multcomplex . ((sqrcomplex . x1),(sqrcomplex . x2)) by Def1 ; :: thesis: verum