theorem :: INTEGR26:31

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 & ( for x being set st x in I holds
G . x <> 0 ) holds
F / G is_antiderivative_of ((f (#) G) - (F (#) g)) / (G (#) G),I