let x0 be positive Real; :: thesis: for f being Element of the carrier of (Polynom-Ring INT.Ring) holds 'F' f is_differentiable_on ].0,x0.[
let f be Element of the carrier of (Polynom-Ring INT.Ring); :: thesis: 'F' f is_differentiable_on ].0,x0.[
set F = 'F' f;
set Z = ].0,x0.[;
A1: dom ('F' f) = REAL by Lm23;
'F' f is_differentiable_on REAL by Lm25;
then for x being Real st x in ].0,x0.[ holds
'F' f is_differentiable_in x ;
hence 'F' f is_differentiable_on ].0,x0.[ by A1, FDIFF_1:9; :: thesis: verum