let A be complex-membered set ; :: thesis: for a, b being complex number holds (a + b) /// A c= (a /// A) ++ (b /// A)
let a, b be complex number ; :: 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