let p be Polynomial of F_Real; :: thesis: Eval (Leading-Monomial p) = FPower ((p . ((len p) -' 1)),((len p) -' 1))
set l = Leading-Monomial p;
set m = (len p) -' 1;
reconsider f = FPower ((p . ((len p) -' 1)),((len p) -' 1)) as Function of REAL,REAL ;
Eval (Leading-Monomial p) = f

proof

let r be Element of REAL ; :: according to FUNCT_2:def 8 :: thesis: (Eval (Leading-Monomial p)) . r = f . r
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
.= f . r by POLYNOM5:def 12 ; :: thesis: verum

end;

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