let f be Element of the carrier of (Polynom-Ring INT.Ring); :: thesis: 'F' f is_differentiable_on REAL
'F' f is_differentiable_on dom ('F' f) by FDIFF_1:def 8;
hence 'F' f is_differentiable_on REAL by Lm23; :: thesis: verum