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

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