let x be object ; :: thesis: ( x in dom (Poly-INT fp) implies (Poly-INT fp) . x = fp . 1 )
assume x in dom (Poly-INT fp) ; :: thesis: (Poly-INT fp) . x = fp . 1
then reconsider x = x as Element of INT ;
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