let n be Nat; :: thesis: for r being Element of F_Real holds Eval (seq (n,r)) = r (#) (#Z n)
let r be Element of F_Real; :: thesis: Eval (seq (n,r)) = r (#) (#Z n)
let a be Element of REAL ; :: according to FUNCT_2:def 8 :: thesis: (Eval (seq (n,r))) . a = (r (#) (#Z n)) . a
set p = seq (n,r);
set x = In (a,F_Real);
A1: (seq (n,r)) . n = r by Th24;
A2: power ((In (a,F_Real)),n) = (#Z n) . a by Th43;
thus (Eval (seq (n,r))) . a = eval ((seq (n,r)),(In (a,F_Real))) by POLYNOM5:def 13
.= ((seq (n,r)) . n) * (power ((In (a,F_Real)),n)) by Th38
.= (r (#) (#Z n)) . a by A1, A2, VALUED_1:6 ; :: thesis: verum