theorem :: INTEGR26:30

for f, g, F, G being PartFunc of REAL,REAL
for I being non empty Interval st F is_antiderivative_of f,I & G is_antiderivative_of g,I holds
F (#) G is_antiderivative_of (f (#) G) + (F (#) g),I