let fp be FinSequence of INT ; :: thesis: ( len fp = 1 implies for x being Element of INT holds (Poly-INT fp) . x = fp . 1 )
assume A1: len fp = 1 ; :: thesis: for x being Element of INT holds (Poly-INT fp) . x = fp . 1
let x be Element of INT ; :: thesis: (Poly-INT fp) . x = fp . 1
consider fr being FinSequence of INT such that
A2: len fr = len fp and
A3: for d being Nat st d in dom fr holds
fr . d = (fp . d) * (x |^ (d -' 1)) and
A4: (Poly-INT fp) . x = Sum fr by Def1;
1 in dom fr by A1, A2, FINSEQ_3:25;
then A5: fr . 1 = (fp . 1) * (x |^ (1 -' 1)) by A3
.= (fp . 1) * (x |^ 0) by XREAL_1:232
.= (fp . 1) * 1 by NEWTON:4 ;
fr = <*(fr . 1)*> by A1, A2, FINSEQ_1:40;
hence (Poly-INT fp) . x = fp . 1 by A4, A5, RVSUM_1:73; :: thesis: verum