theorem Th8: :: HILB10_4:8

for cF1, cF2 being complex-valued XFinSequence
for c being Complex holds c + (cF1 ^ cF2) = (c + cF1) ^ (c + cF2)