let A be complex-membered set ; :: thesis: for a, b being Complex holds (a + b) ** A c= (a ** A) ++ (b ** A)
let a, b be Complex; :: thesis: (a + b) ** A c= (a ** A) ++ (b ** A)
{a} ++ {b} = {(a + b)} by Th51;
hence (a + b) ** A c= (a ** A) ++ (b ** A) by Th95; :: thesis: verum