let n be Nat; :: thesis: 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)
let p be object ; :: thesis: ( p in n implies 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) )
assume A1: p in n ; :: thesis: 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)
let i be integer Element of F_Real; :: thesis: for x being Function of n,F_Real holds eval ((Monom (i,((EmptyBag n) +* (p,1)))),x) = i * (x /. p)
let x be Function of n,F_Real; :: thesis: eval ((Monom (i,((EmptyBag n) +* (p,1)))),x) = i * (x /. p)
set Ep = (EmptyBag n) +* (p,1);
n = dom x by PARTFUN1:def 2;
then A2: x . p = x /. p by A1, PARTFUN1:def 6;
eval (((EmptyBag n) +* (p,1)),x) = (power F_Real) . ((x . p),1) by A1, Th14
.= x /. p by A2, GROUP_1:50 ;
hence eval ((Monom (i,((EmptyBag n) +* (p,1)))),x) = i * (x /. p) by POLYNOM7:13; :: thesis: verum