let A be complex-membered set ; :: thesis: for a, b being Complex holds (a * b) ** A = a ** (b ** A)
let a, b be Complex; :: thesis: (a * b) ** A = a ** (b ** A)
thus (a * b) ** A = ({a} ** {b}) ** A by Th98
.= a ** (b ** A) by Th90 ; :: thesis: verum