let p be Polynomial of F_Real; :: thesis:
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))

let r be Element of REAL ; :: according to FUNCT_2:def 8 :: thesis:
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:

end;