theorem Th27: :: LPSPACC1:27

for a being Complex
for X being non empty set holds
( (X --> 0c) + (X --> 0c) = X --> 0c & a (#) (X --> 0c) = X --> 0c )