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 S₁[ Nat] means for p being Polynomial of F_Real st len p <= $1 holds
(Eval p) `| = Eval (poly_diff p);
A1: S₁[ 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 S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A4: S₁[n] ; :: thesis: S₁[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 S₁[n] from NAT_1:sch 2(A1, A3);
len p = len p ;
hence (Eval p) `| = Eval (poly_diff p) by A11; :: thesis: verum