let f, F be PartFunc of REAL,REAL; :: thesis: for I being non empty Interval
for r being Real st F is_antiderivative_of f,I holds
r (#) F is_antiderivative_of r (#) f,I
let I be non empty Interval; :: thesis: for r being Real st F is_antiderivative_of f,I holds
r (#) F is_antiderivative_of r (#) f,I
let r be Real; :: thesis: ( F is_antiderivative_of f,I implies r (#) F is_antiderivative_of r (#) f,I )
assume A1: F is_antiderivative_of f,I ; :: thesis: r (#) F is_antiderivative_of r (#) f,I
then ( r (#) F is_differentiable_on_interval I & (r (#) F) `\ I = r (#) (F `\ I) ) by FDIFF_12:23;
hence r (#) F is_antiderivative_of r (#) f,I by A1, RFUNCT_1:49; :: thesis: verum