let f, g, F, G be PartFunc of REAL,REAL; :: thesis: 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
let I be non empty Interval; :: thesis: ( F is_antiderivative_of f,I & G is_antiderivative_of g,I implies F (#) G is_antiderivative_of (f (#) G) + (F (#) g),I )
assume that
A1: F is_antiderivative_of f,I and
A2: G is_antiderivative_of g,I ; :: thesis: F (#) G is_antiderivative_of (f (#) G) + (F (#) g),I
A3: (F (#) G) `\ I = (G (#) (F `\ I)) + (F (#) (G `\ I)) by A1, A2, FDIFF_12:24;
( G (#) (F `\ I) = (G (#) f) | I & F (#) (G `\ I) = (F (#) g) | I ) by A1, A2, RFUNCT_1:45;
hence F (#) G is_antiderivative_of (f (#) G) + (F (#) g),I by A3, A1, A2, FDIFF_12:24, RFUNCT_1:44; :: thesis: verum