let p be Element of the carrier of (Polynom-Ring F_Real); :: thesis: (Eval (~ p)) `| = Eval (~ ((Der1 F_Real) . p))
set DR = Der1 F_Real;
set f = (Eval (~ p)) `| ;
set g = Eval (~ ((Der1 F_Real) . p));
defpred S₁[ Nat] means for p being Element of the carrier of (Polynom-Ring F_Real) st len (~ p) <= $1 holds
(Eval (~ p)) `| = Eval (~ ((Der1 F_Real) . p));
A1: S₁[ 0 ]

proof

let p be Element of the carrier of (Polynom-Ring F_Real); :: thesis: ( len (~ p) <= 0 implies (Eval (~ p)) `| = Eval (~ ((Der1 F_Real) . p)) )
assume len (~ p) <= 0 ; :: thesis: (Eval (~ p)) `| = Eval (~ ((Der1 F_Real) . p))
then A3: len (~ p) = 0 ;
then A4: p = 0_. F_Real by POLYNOM4:5;
A5: ~ p = 0_. F_Real by A3, POLYNOM4:5;
~ ((Der1 F_Real) . p) = 0_. F_Real by A4, FIELD_14:58;
hence (Eval (~ p)) `| = Eval (~ ((Der1 F_Real) . p)) by POLYDIFF:52, A5, POLYDIFF:54; :: thesis: verum

end;

A7: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A8: S₁[n] ; :: thesis: S₁[n + 1]
let p be Element of the carrier of (Polynom-Ring F_Real); :: thesis: ( len (~ p) <= n + 1 implies (Eval (~ p)) `| = Eval (~ ((Der1 F_Real) . p)) )
assume A9: len (~ p) <= n + 1 ; :: thesis: (Eval (~ p)) `| = Eval (~ ((Der1 F_Real) . p))
set m = (len (~ p)) -' 1;
set q = @ ((~ p) || ((len (~ p)) -' 1));

A11: 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 A9, XXREAL_0:2, POLYDIFF:36; :: 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;

set l = Leading-Monomial (~ p);
A13: Der1 F_Real is additive ;
A14: ~ ((Der1 F_Real) . (@ ((Leading-Monomial (~ p)) + (~ (@ ((~ p) || ((len (~ p)) -' 1))))))) = (Der1 F_Real) . ((@ (~ (@ ((~ p) || ((len (~ p)) -' 1))))) + (@ (Leading-Monomial (~ p)))) by POLYNOM3:def 10
.= ~ (((Der1 F_Real) . (@ (~ (@ ((~ p) || ((len (~ p)) -' 1)))))) + ((Der1 F_Real) . (@ (Leading-Monomial (~ p))))) by A13
.= (~ ((Der1 F_Real) . (@ (LM (~ p))))) + (~ ((Der1 F_Real) . (@ ((~ p) || ((len (~ p)) -' 1))))) by POLYNOM3:def 10 ;
A15: ( @ ((~ (@ ((~ p) || ((len (~ p)) -' 1)))) + (Leading-Monomial (~ p))) = @ (~ p) & @ (~ p) = p ) by POLYDIFF:37;
A16: (Eval (LM (~ p))) `| = Eval (~ ((Der1 F_Real) . (@ (LM (~ p))))) by Lm22;
(Eval (~ p)) `| = (Eval ((~ (@ ((~ p) || ((len (~ p)) -' 1)))) + (LM (~ p)))) `| by POLYDIFF:37
.= ((Eval (~ (@ ((~ p) || ((len (~ p)) -' 1))))) + (Eval (LM (~ p)))) `| by POLYDIFF:55
.= ((Eval (~ (@ ((~ p) || ((len (~ p)) -' 1))))) `|) + ((Eval (LM (~ p))) `|) by POLYDIFF:14
.= (Eval (~ ((Der1 F_Real) . (@ (LM (~ p)))))) + (Eval (~ ((Der1 F_Real) . (@ ((~ p) || ((len (~ p)) -' 1)))))) by A8, A11, NAT_1:13, A16
.= Eval (~ ((Der1 F_Real) . p)) by A14, A15, POLYDIFF:55 ;
hence (Eval (~ p)) `| = Eval (~ ((Der1 F_Real) . p)) ; :: thesis: verum

end;

A17: for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A7);
len (~ p) = len (~ p) ;
hence (Eval (~ p)) `| = Eval (~ ((Der1 F_Real) . p)) by A17; :: thesis: verum