let p be prime odd Nat; :: thesis: for m being positive Nat
for g being non zero Polynomial of INT.Ring st deg g = m holds
for x being non zero Element of F_Real holds Sum (delta_2 (m,p,g,x)) = ((g . 0) * (('F' (f_0 (m,p))) . 0)) - ((Ext_eval (g,x)) * (('F' (f_0 (m,p))) . 0))
let m be positive Nat; :: thesis: for g being non zero Polynomial of INT.Ring st deg g = m holds
for x being non zero Element of F_Real holds Sum (delta_2 (m,p,g,x)) = ((g . 0) * (('F' (f_0 (m,p))) . 0)) - ((Ext_eval (g,x)) * (('F' (f_0 (m,p))) . 0))
let g be non zero Polynomial of INT.Ring; :: thesis: ( deg g = m implies for x being non zero Element of F_Real holds Sum (delta_2 (m,p,g,x)) = ((g . 0) * (('F' (f_0 (m,p))) . 0)) - ((Ext_eval (g,x)) * (('F' (f_0 (m,p))) . 0)) )
assume deg g = m ; :: thesis: for x being non zero Element of F_Real holds Sum (delta_2 (m,p,g,x)) = ((g . 0) * (('F' (f_0 (m,p))) . 0)) - ((Ext_eval (g,x)) * (('F' (f_0 (m,p))) . 0))
then A2: len g = m + 1 ;
for x being non zero Element of F_Real holds Sum (delta_2 (m,p,g,x)) = ((g . 0) * (('F' (f_0 (m,p))) . 0)) - ((Ext_eval (g,x)) * (('F' (f_0 (m,p))) . 0))

proof

let x be non zero Element of F_Real; :: thesis: Sum (delta_2 (m,p,g,x)) = ((g . 0) * (('F' (f_0 (m,p))) . 0)) - ((Ext_eval (g,x)) * (('F' (f_0 (m,p))) . 0))
A3: (power F_Real) . (x,0) = x |^ 0 by BINOM:def 2
.= 1_ F_Real by BINOM:8 ;
reconsider r = - ((g . 0) * (('F' (f_0 (m,p))) . 0)) as Element of F_Real by XREAL_0:def 1;
A4: Sum (<*r*> ^ (delta_2 (m,p,g,x))) = r + (Sum (delta_2 (m,p,g,x))) by FVSUM_1:72;
set F = <*r*> ^ (delta_2 (m,p,g,x));
consider u being Element of INT.Ring such that
A5: ('F' (f_0 (m,p))) . 0 = (((p -' 1) !) * (In (((((- 1) |^ m) * (m !)) |^ p),INT.Ring))) + ((In ((p !),INT.Ring)) * u) by Th33;
reconsider s = ('F' (f_0 (m,p))) . 0 as Element of INT.Ring by A5;
A6: ( len <*r*> = 1 & len (delta_2 (m,p,g,x)) = m ) by Def6, FINSEQ_1:39;
len (<*r*> ^ (delta_2 (m,p,g,x))) = 1 + m by A6, FINSEQ_1:22;
then A8: dom (<*r*> ^ (delta_2 (m,p,g,x))) = Seg (m + 1) by FINSEQ_1:def 3;
A9: dom (delta_2 (m,p,g,x)) = Seg m by A6, FINSEQ_1:def 3;
A10: for n being Element of NAT st n in dom (<*r*> ^ (delta_2 (m,p,g,x))) holds
(<*r*> ^ (delta_2 (m,p,g,x))) . n = - (((s * g) . (n -' 1)) * ((power F_Real) . (x,(n -' 1))))

proof

let n be Element of NAT ; :: thesis: ( n in dom (<*r*> ^ (delta_2 (m,p,g,x))) implies (<*r*> ^ (delta_2 (m,p,g,x))) . n = - (((s * g) . (n -' 1)) * ((power F_Real) . (x,(n -' 1)))) )
assume A11: n in dom (<*r*> ^ (delta_2 (m,p,g,x))) ; :: thesis: (<*r*> ^ (delta_2 (m,p,g,x))) . n = - (((s * g) . (n -' 1)) * ((power F_Real) . (x,(n -' 1))))

per cases ( n = 1 or n <> 1 ) ;

suppose A12: n = 1 ; :: thesis: (<*r*> ^ (delta_2 (m,p,g,x))) . n = - (((s * g) . (n -' 1)) * ((power F_Real) . (x,(n -' 1))))

then n -' 1 = 0 by XREAL_1:232;
then (<*r*> ^ (delta_2 (m,p,g,x))) . n = - ((s * (g . (n -' 1))) * ((power F_Real) . (x,(n -' 1)))) by A3, A12;
hence (<*r*> ^ (delta_2 (m,p,g,x))) . n = - (((s * g) . (n -' 1)) * ((power F_Real) . (x,(n -' 1)))) by POLYNOM5:def 4; :: thesis: verum

end;

suppose A14: n <> 1 ; :: thesis: (<*r*> ^ (delta_2 (m,p,g,x))) . n = - (((s * g) . (n -' 1)) * ((power F_Real) . (x,(n -' 1))))

A15: ( 1 <= n & n <= m + 1 ) by A8, A11, FINSEQ_1:1;
then A16: ( (len <*r*>) + 1 <= n & n <= (len <*r*>) + (len (delta_2 (m,p,g,x))) ) by A6, NAT_1:23, A14;
set n1 = n -' 1;
A17: 2 - 1 <= n - 1 by NAT_1:23, A14, A15, XREAL_1:9;
n - 1 <= (m + 1) - 1 by A15, XREAL_1:9;
then ( 1 <= n -' 1 & n -' 1 <= m ) by XREAL_1:233, A15, A17;
then A19: n -' 1 in dom (delta_2 (m,p,g,x)) by A9;
(<*r*> ^ (delta_2 (m,p,g,x))) . n = (delta_2 (m,p,g,x)) . (n - 1) by A16, A6, FINSEQ_1:23
.= (delta_2 (m,p,g,x)) . (n -' 1) by XREAL_1:233, A15
.= - ((g . (n -' 1)) * (((power F_Real) . (x,(n -' 1))) * s)) by A19, Def6
.= - ((s * (g . (n -' 1))) * ((power F_Real) . (x,(n -' 1)))) ;
hence (<*r*> ^ (delta_2 (m,p,g,x))) . n = - (((s * g) . (n -' 1)) * ((power F_Real) . (x,(n -' 1)))) by POLYNOM5:def 4; :: thesis: verum

end;

end;

end;

per cases ( s = 0 or s <> 0 ) ;

suppose A20: s = 0 ; :: thesis: Sum (delta_2 (m,p,g,x)) = ((g . 0) * (('F' (f_0 (m,p))) . 0)) - ((Ext_eval (g,x)) * (('F' (f_0 (m,p))) . 0))

A21: for i being Nat st i in dom (delta_2 (m,p,g,x)) holds
(delta_2 (m,p,g,x)) . i = ((Seg m) --> 0) . i

proof

let i be Nat; :: thesis: ( i in dom (delta_2 (m,p,g,x)) implies (delta_2 (m,p,g,x)) . i = ((Seg m) --> 0) . i )
assume i in dom (delta_2 (m,p,g,x)) ; :: thesis: (delta_2 (m,p,g,x)) . i = ((Seg m) --> 0) . i
then (delta_2 (m,p,g,x)) . i = - ((g . i) * (((power F_Real) . (x,i)) * (0. INT.Ring))) by A20, Def6;
hence (delta_2 (m,p,g,x)) . i = ((Seg m) --> 0) . i ; :: thesis: verum

end;

delta_2 (m,p,g,x) = m |-> (0. F_Real) by A21, A6, FINSEQ_1:def 3;
hence Sum (delta_2 (m,p,g,x)) = ((g . 0) * (('F' (f_0 (m,p))) . 0)) - ((Ext_eval (g,x)) * (('F' (f_0 (m,p))) . 0)) by MATRIX_3:11, A20; :: thesis: verum

end;

suppose s <> 0 ; :: thesis: Sum (delta_2 (m,p,g,x)) = ((g . 0) * (('F' (f_0 (m,p))) . 0)) - ((Ext_eval (g,x)) * (('F' (f_0 (m,p))) . 0))

then reconsider s0 = - s as non zero Element of INT.Ring by STRUCT_0:def 12;
(- s) * g is Polynomial of INT.Ring ;
then reconsider h = - (s * g) as Polynomial of INT.Ring by HURWITZ:15;
A25: deg (s0 * g) = deg g by RING_5:4;
reconsider h0 = s0 * g as Polynomial of F_Real by FIELD_4:9, LIOUVIL2:5;
deg (~ (@ (s0 * g))) = deg (~ (@ h0)) by FIELD_4:20;
then A28: len (<*r*> ^ (delta_2 (m,p,g,x))) = len h0 by A25, A2, A6, FINSEQ_1:22;
A29: for n being Element of NAT st n in dom (<*r*> ^ (delta_2 (m,p,g,x))) holds
(<*r*> ^ (delta_2 (m,p,g,x))) . n = (h0 . (n -' 1)) * ((power F_Real) . (x,(n -' 1)))

proof

let n be Element of NAT ; :: thesis: ( n in dom (<*r*> ^ (delta_2 (m,p,g,x))) implies (<*r*> ^ (delta_2 (m,p,g,x))) . n = (h0 . (n -' 1)) * ((power F_Real) . (x,(n -' 1))) )
assume n in dom (<*r*> ^ (delta_2 (m,p,g,x))) ; :: thesis: (<*r*> ^ (delta_2 (m,p,g,x))) . n = (h0 . (n -' 1)) * ((power F_Real) . (x,(n -' 1)))
then (<*r*> ^ (delta_2 (m,p,g,x))) . n = - (((s * g) . (n -' 1)) * ((power F_Real) . (x,(n -' 1)))) by A10
.= - ((s * (g . (n -' 1))) * ((power F_Real) . (x,(n -' 1)))) by POLYNOM5:def 4
.= (s0 * (g . (n -' 1))) * ((power F_Real) . (x,(n -' 1))) ;
hence (<*r*> ^ (delta_2 (m,p,g,x))) . n = (h0 . (n -' 1)) * ((power F_Real) . (x,(n -' 1))) by POLYNOM5:def 4; :: thesis: verum

end;

reconsider s1 = s0 as Element of F_Real by XREAL_0:def 1;
eval (h0,x) = eval ((~ (@ h0)),x)
.= Ext_eval ((~ (@ (s0 * g))),x) by FIELD_4:26
.= s1 * (Ext_eval (g,x)) by E_TRANS1:36 ;
then Sum (<*r*> ^ (delta_2 (m,p,g,x))) = - ((('F' (f_0 (m,p))) . 0) * (Ext_eval (g,x))) by A29, A28, POLYNOM4:def 2;
hence Sum (delta_2 (m,p,g,x)) = ((g . 0) * (('F' (f_0 (m,p))) . 0)) - ((Ext_eval (g,x)) * (('F' (f_0 (m,p))) . 0)) by A4; :: thesis: verum

end;

end;

end;

hence for x being non zero Element of F_Real holds Sum (delta_2 (m,p,g,x)) = ((g . 0) * (('F' (f_0 (m,p))) . 0)) - ((Ext_eval (g,x)) * (('F' (f_0 (m,p))) . 0)) ; :: thesis: verum