let fp be FinSequence of INT ; :: thesis: ( len fp = 1 implies Poly-INT fp = INT --> (fp . 1) )
assume A1: len fp = 1 ; :: thesis: Poly-INT fp = INT --> (fp . 1)
for x being object st x in dom (Poly-INT fp) holds
(Poly-INT fp) . x = fp . 1

proof

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

end;

then Poly-INT fp = (dom (Poly-INT fp)) --> (fp . 1) by FUNCOP_1:11;
hence Poly-INT fp = INT --> (fp . 1) by FUNCT_2:def 1; :: thesis: verum