set PRI = Polynom-Ring INT.Ring;
set PRR = Polynom-Ring F_Real;
let x0 be Element of INT.Ring; :: thesis: for x being Element of F_Real
for F being FinSequence of the carrier of (Polynom-Ring INT.Ring) st x = x0 holds
(Eval (~ (^ (Sum F)))) . x = Sum (eval (F,x0))
let x be Element of F_Real; :: thesis: for F being FinSequence of the carrier of (Polynom-Ring INT.Ring) st x = x0 holds
(Eval (~ (^ (Sum F)))) . x = Sum (eval (F,x0))
let F be FinSequence of the carrier of (Polynom-Ring INT.Ring); :: thesis: ( x = x0 implies (Eval (~ (^ (Sum F)))) . x = Sum (eval (F,x0)) )
assume A1: x = x0 ; :: thesis: (Eval (~ (^ (Sum F)))) . x = Sum (eval (F,x0))
reconsider erFx = eval ((^ F),x) as FinSequence of F_Real ;
reconsider eIFx = eval (F,x0) as FinSequence of INT.Ring ;
A2: erFx = eIFx by A1, Th28;
(Eval (~ (^ (Sum F)))) . x = eval ((~ (^ (Sum F))),x) by POLYNOM5:def 13
.= eval ((~ (Sum (^ F))),x) by Th29
.= Sum (eval ((^ F),x)) by Th26
.= In ((Sum eIFx),F_Real) by A2, LIOUVIL2:5, ALGNUM_1:10 ;
hence (Eval (~ (^ (Sum F)))) . x = Sum (eval (F,x0)) ; :: thesis: verum