let p be Element of the carrier of (Polynom-Ring F_Real); :: thesis: (Eval (LM (~ p))) `| = Eval (~ ((Der1 F_Real) . (@ (LM (~ p)))))
set F = F_Real ;
set DR = Der1 F_Real;
set l = Leading-Monomial (~ p);
set m = (len (~ p)) -' 1;
set k = (len (~ p)) -' 2;
reconsider f = FPower (((~ p) . ((len (~ p)) -' 1)),((len (~ p)) -' 1)) as Function of REAL,REAL ;
reconsider a = ((~ p) . ((len (~ p)) -' 1)) * ((len (~ p)) -' 1) as Element of F_Real ;
( len (~ p) <= 2 - 1 or len (~ p) >= 2 ) by INT_1:52;

per cases then ( len (~ p) = 0 or len (~ p) = 1 or 2 <= len (~ p) ) by NAT_1:25;

suppose A1: ( len (~ p) = 0 or len (~ p) = 1 ) ; :: thesis: (Eval (LM (~ p))) `| = Eval (~ ((Der1 F_Real) . (@ (LM (~ p)))))

then A2: ( ~ p = 0_. F_Real or ~ p = <%((~ p) . 0)%> ) by ALGSEQ_1:def 5;
( len (LM (~ p)) = 0 or len (LM (~ p)) = 1 ) by A1, POLYNOM4:15;
then ( deg (LM (~ p)) = - 1 or deg (LM (~ p)) = 0 ) ;
then @ (LM (~ p)) is constant ;
then (Der1 F_Real) . (@ (LM (~ p))) = 0_. F_Real by FIELD_14:60;
then Eval (~ ((Der1 F_Real) . (@ (LM (~ p))))) = REAL --> 0 by POLYDIFF:52;
hence (Eval (LM (~ p))) `| = Eval (~ ((Der1 F_Real) . (@ (LM (~ p))))) by A2, POLYDIFF:54; :: thesis: verum

end;

suppose A4: 2 <= len (~ p) ; :: thesis: (Eval (LM (~ p))) `| = Eval (~ ((Der1 F_Real) . (@ (LM (~ p)))))

then A5: (len (~ p)) -' 2 = (len (~ p)) - 2 by XREAL_1:233
.= ((len (~ p)) - 1) - 1
.= ((len (~ p)) -' 1) - 1 by A4, XXREAL_0:2, XREAL_1:233 ;
A6: Eval (Leading-Monomial (~ p)) = ((~ p) . ((len (~ p)) -' 1)) (#) (#Z ((len (~ p)) -' 1)) by POLYDIFF:59;
reconsider c1 = (~ p) . ((len (~ p)) -' 1) as Real ;
reconsider c2 = (len (~ p)) -' 1 as Nat ;
reconsider h = #Z ((len (~ p)) -' 2) as real-valued Function ;
A7: ((~ p) . ((len (~ p)) -' 1)) (#) ((#Z ((len (~ p)) -' 1)) `|) = ((~ p) . ((len (~ p)) -' 1)) (#) (((len (~ p)) -' 1) (#) (#Z ((len (~ p)) -' 2))) by A5, POLYDIFF:13
.= c1 (#) (((len (~ p)) -' 1) (#) (FPower ((1. F_Real),((len (~ p)) -' 2)))) by POLYDIFF:40
.= (c1 * ((len (~ p)) -' 1)) (#) (FPower ((1. F_Real),((len (~ p)) -' 2))) by RFUNCT_1:17 ;
(((len (~ p)) -' 1) * ((~ p) . ((len (~ p)) -' 1))) (#) (#Z ((len (~ p)) -' 2)) = (((len (~ p)) -' 1) * ((~ p) . ((len (~ p)) -' 1))) (#) (FPower ((1. F_Real),((len (~ p)) -' 2))) by POLYDIFF:40
.= (c1 * ((len (~ p)) -' 1)) (#) (FPower ((1. F_Real),((len (~ p)) -' 2))) by Lm20 ;
then A8: (((len (~ p)) -' 1) * ((~ p) . ((len (~ p)) -' 1))) (#) (#Z ((len (~ p)) -' 2)) = (Eval (Leading-Monomial (~ p))) `| by A6, A7, POLYDIFF:19;
(Der1 F_Real) . (@ (LM (~ p))) = seq (((len (~ p)) -' 2),a) by Lm21;
then Eval (~ ((Der1 F_Real) . (@ (LM (~ p))))) = (((~ p) . ((len (~ p)) -' 1)) * ((len (~ p)) -' 1)) (#) (#Z ((len (~ p)) -' 2)) by POLYDIFF:60;
hence (Eval (LM (~ p))) `| = Eval (~ ((Der1 F_Real) . (@ (LM (~ p))))) by A8, BINOM:18; :: thesis: verum

end;

end;