let x0 be positive Real; :: thesis: for f being Element of the carrier of (Polynom-Ring INT.Ring) ex s being Real st
( 0 < s & s < 1 & (exp_R1 (#) ('F' f)) . x0 = ((exp_R1 (#) ('F' f)) . 0) + (x0 * (diff ((exp_R1 (#) ('F' f)),(s * x0)))) )
let f be Element of the carrier of (Polynom-Ring INT.Ring); :: thesis: ex s being Real st
( 0 < s & s < 1 & (exp_R1 (#) ('F' f)) . x0 = ((exp_R1 (#) ('F' f)) . 0) + (x0 * (diff ((exp_R1 (#) ('F' f)),(s * x0)))) )
[.0,x0.] c= REAL ;
then A1: [.0,x0.] c= dom (exp_R1 (#) ('F' f)) by FUNCT_2:def 1;
A2: (exp_R1 (#) ('F' f)) | [.0,x0.] is continuous by Th32;
exp_R1 (#) ('F' f) is_differentiable_on ].0,x0.[ by Th33;
then ex s being Real st
( 0 < s & s < 1 & (exp_R1 (#) ('F' f)) . (0 + x0) = ((exp_R1 (#) ('F' f)) . 0) + (x0 * (diff ((exp_R1 (#) ('F' f)),(0 + (s * x0))))) ) by A1, A2, ROLLE:4;
hence ex s being Real st
( 0 < s & s < 1 & (exp_R1 (#) ('F' f)) . x0 = ((exp_R1 (#) ('F' f)) . 0) + (x0 * (diff ((exp_R1 (#) ('F' f)),(s * x0)))) ) ; :: thesis: verum