let x0 be positive Real; :: thesis: for f being Element of the carrier of (Polynom-Ring INT.Ring) holds exp_R1 (#) ('F' f) is_differentiable_on ].0,x0.[
let f be Element of the carrier of (Polynom-Ring INT.Ring); :: thesis: exp_R1 (#) ('F' f) is_differentiable_on ].0,x0.[
set f1 = exp_R ^ ;
set f2 = 'F' f;
set Z = ].0,x0.[;
A1: ( dom (exp_R ^) = REAL & dom ('F' f) = REAL ) by Lm23A, Lm23;
A2: exp_R ^ is_differentiable_on ].0,x0.[ by Lm31;
A3: 'F' f is_differentiable_on ].0,x0.[ by Lm32;
dom ((exp_R ^) (#) ('F' f)) = (dom (exp_R ^)) /\ (dom ('F' f)) by VALUED_1:def 4
.= REAL by A1 ;
hence exp_R1 (#) ('F' f) is_differentiable_on ].0,x0.[ by A2, A3, FDIFF_1:21; :: thesis: verum