theorem Th142: :: MEMBER_1:142

for A being complex-membered set
for a being Complex holds a ++ A = { (a + c) where c is Complex : c in A }