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