let p be Polynomial of F_Real; :: thesis: (Eval p) `| = Eval (poly_diff p)
set f = (Eval p) `| ;
set g = Eval (poly_diff p);
defpred S1[ Nat] means for p being Polynomial of F_Real st len p <= $1 holds
(Eval p) `| = Eval (poly_diff p);
A1: S1[ 0 ]
proof
let p be Polynomial of F_Real; :: thesis: ( len p <= 0 implies (Eval p) `| = Eval (poly_diff p) )
assume len p <= 0 ; :: thesis: (Eval p) `| = Eval (poly_diff p)
then len p = 0 ;
then A2: p = 0_. F_Real by POLYNOM4:5;
poly_diff (0_. F_Real) = 0_. F_Real by Th46;
hence (Eval p) `| = Eval (poly_diff p) by A2, Th52, Th54; :: thesis: verum
end;
A3: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A4: S1[n] ; :: thesis: S1[n + 1]
let p be Polynomial of F_Real; :: thesis: ( len p <= n + 1 implies (Eval p) `| = Eval (poly_diff p) )
assume A5: len p <= n + 1 ; :: thesis: (Eval p) `| = Eval (poly_diff p)
set m = (len p) -' 1;
set q = p || ((len p) -' 1);
now :: thesis: len (p || ((len p) -' 1)) < n + 1
per cases ( p <> 0_. F_Real or p = 0_. F_Real ) ;
suppose p <> 0_. F_Real ; :: thesis: len (p || ((len p) -' 1)) < n + 1
hence len (p || ((len p) -' 1)) < n + 1 by A5, Th36, XXREAL_0:2; :: thesis: verum
end;
suppose p = 0_. F_Real ; :: thesis: len (p || ((len p) -' 1)) < n + 1
hence len (p || ((len p) -' 1)) < n + 1 by POLYNOM4:3; :: thesis: verum
end;
end;
end;
then A6: (Eval (p || ((len p) -' 1))) `| = Eval (poly_diff (p || ((len p) -' 1))) by A4, NAT_1:13;
set l = Leading-Monomial p;
A7: (p || ((len p) -' 1)) + (Leading-Monomial p) = p by Th37;
A8: poly_diff ((p || ((len p) -' 1)) + (Leading-Monomial p)) = (poly_diff (p || ((len p) -' 1))) + (poly_diff (Leading-Monomial p)) by Th47;
A9: (Eval (Leading-Monomial p)) `| = Eval (poly_diff (Leading-Monomial p)) by Lm3;
A10: Eval ((poly_diff (p || ((len p) -' 1))) + (poly_diff (Leading-Monomial p))) = (Eval (poly_diff (p || ((len p) -' 1)))) + (Eval (poly_diff (Leading-Monomial p))) by Th55;
Eval ((p || ((len p) -' 1)) + (Leading-Monomial p)) = (Eval (p || ((len p) -' 1))) + (Eval (Leading-Monomial p)) by Th55;
hence (Eval p) `| = Eval (poly_diff p) by A6, A7, A8, A9, A10, Th14; :: thesis: verum
end;
A11: for n being Nat holds S1[n] from NAT_1:sch 2(A1, A3);
 len p = len p ;
hence (Eval p) `| = Eval (poly_diff p) by A11; :: thesis: verum