let p be Polynomial of F_Real; :: thesis: Eval (Leading-Monomial p) = (p . ((len p) -' 1)) (#) (#Z ((len p) -' 1))
set l = Leading-Monomial p;
set m = (len p) -' 1;
set f = (p . ((len p) -' 1)) (#) (#Z ((len p) -' 1));
Eval (Leading-Monomial p) = (p . ((len p) -' 1)) (#) (#Z ((len p) -' 1))

proof

let r be Element of REAL ; :: according to FUNCT_2:def 8 :: thesis: (Eval (Leading-Monomial p)) . r = ((p . ((len p) -' 1)) (#) (#Z ((len p) -' 1))) . r
A1: power ((In (r,F_Real)),((len p) -' 1)) = r |^ ((len p) -' 1) by Th39
.= r #Z ((len p) -' 1) by PREPOWER:36
.= (#Z ((len p) -' 1)) . r by TAYLOR_1:def 1 ;
thus (Eval (Leading-Monomial p)) . r = eval ((Leading-Monomial p),(In (r,F_Real))) by POLYNOM5:def 13
.= (p . ((len p) -' 1)) * (power ((In (r,F_Real)),((len p) -' 1))) by POLYNOM4:22
.= ((p . ((len p) -' 1)) (#) (#Z ((len p) -' 1))) . r by A1, VALUED_1:6 ; :: thesis: verum

end;

hence Eval (Leading-Monomial p) = (p . ((len p) -' 1)) (#) (#Z ((len p) -' 1)) ; :: thesis: verum