let p be Polynomial of F_Real; :: thesis:
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 by XREAL_0:def 1;
A1: poly_diff (Leading-Monomial p) = seq (((len p) -' 2),a) by Th50;
A2: (#Z ((len p) -' 1)) `| = ((len p) -' 1) (#) (#Z (((len p) -' 1) - 1)) by Th13;
( len p <= 2 - 1 or len p >= 2 ) by INT_1:52;

per cases by NAT_1:25;

suppose ( len p = 0 or len p = 1 ) ; :: thesis:

then A3: ( p = 0_. F_Real or p = <%(p . 0)%> ) by ALGSEQ_1:def 5;
then poly_diff (Leading-Monomial p) = 0_. F_Real by Th46;
hence (Eval (Leading-Monomial p)) `| = Eval (poly_diff (Leading-Monomial p)) by A3, Th52, Th54; :: thesis:

end;

suppose A4: 2 <= len p ; :: thesis:

then A5: (len p) -' 2 = (len p) - 2 by XREAL_1:233;
(len p) -' 1 = (len p) - 1 by A4, XXREAL_0:2, XREAL_1:233;
then A6: a (#) (#Z (((len p) -' 1) - 1)) = Eval (seq (((len p) -' 2),a)) by A5, Th60;
Eval (Leading-Monomial p) = (p . ((len p) -' 1)) (#) (#Z ((len p) -' 1)) by Th59;
hence (Eval (Leading-Monomial p)) `| = (p . ((len p) -' 1)) (#) ((#Z ((len p) -' 1)) `|) by Th19
.= Eval (poly_diff (Leading-Monomial p)) by A1, A2, A6, RFUNCT_1:17 ;
:: thesis:

end;

end;