let A be complex-membered set ; :: thesis: for a, b being complex number holds (a + b) ++ A = a ++ (b ++ A)
let a, b be complex number ; :: thesis: (a + b) ++ A = a ++ (b ++ A)
thus (a + b) ++ A = ({a} ++ {b}) ++ A by Th51
.= a ++ (b ++ A) by Th50 ; :: thesis: verum