let f, F, g, G be 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,I & F - G is_antiderivative_of f - g,I )
let I be non empty Interval; ( F is_antiderivative_of f,I & G is_antiderivative_of g,I implies ( F + G is_antiderivative_of f + g,I & F - G is_antiderivative_of f - g,I ) )
assume that
A1:
F is_antiderivative_of f,I
and
A2:
G is_antiderivative_of g,I
; ( F + G is_antiderivative_of f + g,I & F - G is_antiderivative_of f - g,I )
( I c= dom F & I c= dom G )
by A1, A2, FDIFF_12:def 1;
then
I c= (dom F) /\ (dom G)
by XBOOLE_1:19;
then A3:
( I c= dom (F + G) & I c= dom (F - G) )
by VALUED_1:def 1, VALUED_1:12;
then
( (F + G) `\ I = (F `\ I) + (G `\ I) & (F - G) `\ I = (F `\ I) - (G `\ I) )
by A2, A1, FDIFF_12:19, FDIFF_12:20;
hence
( F + G is_antiderivative_of f + g,I & F - G is_antiderivative_of f - g,I )
by A3, A1, A2, RFUNCT_1:44, RFUNCT_1:47, FDIFF_12:19, FDIFF_12:20; verum