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 & ( for d being Nat st d in dom fr holds
fr . d = (fp . d) * (x |^ (d -' 1)) ) & (Poly-INT fp) . x = Sum fr ) by Def1;
A3: fr = <*(fr . 1)*> by A1, A2, FINSEQ_1:57;
1 in dom fr by A1, A2, FINSEQ_3:27;
then fr . 1 = (fp . 1) * (x |^ (1 -' 1)) by A2
.= (fp . 1) * (x |^ 0 ) by XREAL_1:234
.= (fp . 1) * 1 by NEWTON:9 ;
hence (Poly-INT fp) . x = fp . 1 by A2, A3, RVSUM_1:103; :: thesis: verum