for f, g being PartFunc of COMPLEX,COMPLEX
for C being C1-curve st rng C c= dom f & rng C c= dom g & f is_integrable_on C & g is_integrable_on C & f is_bounded_on C & g is_bounded_on C holds
integral ((f + g),C) = (integral (f,C)) + (integral (g,C))