theorem Th3: :: BASEL_1:3

for f, g being complex-valued FinSequence
for c being Complex holds c + (f ^ g) = (c + f) ^ (c + g)