theorem :: E_TRANS1:34

for f being Element of the carrier of (Polynom-Ring INT.Ring)
for x0 being positive Real st len f > 0 holds
ex s being Real st
( 0 < s & s < 1 & (('F' f) . x0) - ((exp_R . x0) * (('F' f) . 0)) = - ((x0 * (exp_R . (x0 * (1 - s)))) * ((Eval (~ (^ f))) . (s * x0))) )