theorem Th27: :: POLYNOM9:27

for n being Nat
for p being object st p in n holds
for i being integer Element of F_Real
for x being Function of n,F_Real holds eval ((Monom (i,((EmptyBag n) +* (p,1)))),x) = i * (x /. p)