defpred S_{1}[ Element of INT , set ] means ex fr being FinSequence of INT st

( len fr = len fp & ( for d being Nat st d in dom fr holds

fr . d = (fp . d) * ($1 |^ (d -' 1)) ) & $2 = Sum fr );

A1: for x being Element of INT ex y being Element of INT st S_{1}[x,y]

A3: for x being Element of INT holds S_{1}[x,f . x]
from FUNCT_2:sch 3(A1);

take f ; :: thesis: for x being Element of INT ex fr being FinSequence of INT st

( len fr = len fp & ( for d being Nat st d in dom fr holds

fr . d = (fp . d) * (x |^ (d -' 1)) ) & f . x = Sum fr )

thus for x being Element of INT ex fr being FinSequence of INT st

( len fr = len fp & ( for d being Nat st d in dom fr holds

fr . d = (fp . d) * (x |^ (d -' 1)) ) & f . x = Sum fr ) by A3; :: thesis: verum

( len fr = len fp & ( for d being Nat st d in dom fr holds

fr . d = (fp . d) * ($1 |^ (d -' 1)) ) & $2 = Sum fr );

A1: for x being Element of INT ex y being Element of INT st S

proof

consider f being Function of INT,INT such that
let x be Element of INT ; :: thesis: ex y being Element of INT st S_{1}[x,y]

deffunc H_{1}( Nat) -> set = (fp . $1) * (x |^ ($1 -' 1));

consider fr being FinSequence such that

A2: ( len fr = len fp & ( for d being Nat st d in dom fr holds

fr . d = H_{1}(d) ) )
from FINSEQ_1:sch 2();

for d being Nat st d in dom fr holds

fr . d in INT

take Sum fr ; :: thesis: S_{1}[x, Sum fr]

take fr ; :: thesis: ( len fr = len fp & ( for d being Nat st d in dom fr holds

fr . d = (fp . d) * (x |^ (d -' 1)) ) & Sum fr = Sum fr )

thus ( len fr = len fp & ( for d being Nat st d in dom fr holds

fr . d = (fp . d) * (x |^ (d -' 1)) ) & Sum fr = Sum fr ) by A2; :: thesis: verum

end;deffunc H

consider fr being FinSequence such that

A2: ( len fr = len fp & ( for d being Nat st d in dom fr holds

fr . d = H

for d being Nat st d in dom fr holds

fr . d in INT

proof

then reconsider fr = fr as FinSequence of INT by FINSEQ_2:12;
let d be Nat; :: thesis: ( d in dom fr implies fr . d in INT )

assume d in dom fr ; :: thesis: fr . d in INT

then fr . d = (fp . d) * (x |^ (d -' 1)) by A2;

hence fr . d in INT by INT_1:def 2; :: thesis: verum

end;assume d in dom fr ; :: thesis: fr . d in INT

then fr . d = (fp . d) * (x |^ (d -' 1)) by A2;

hence fr . d in INT by INT_1:def 2; :: thesis: verum

take Sum fr ; :: thesis: S

take fr ; :: thesis: ( len fr = len fp & ( for d being Nat st d in dom fr holds

fr . d = (fp . d) * (x |^ (d -' 1)) ) & Sum fr = Sum fr )

thus ( len fr = len fp & ( for d being Nat st d in dom fr holds

fr . d = (fp . d) * (x |^ (d -' 1)) ) & Sum fr = Sum fr ) by A2; :: thesis: verum

A3: for x being Element of INT holds S

take f ; :: thesis: for x being Element of INT ex fr being FinSequence of INT st

( len fr = len fp & ( for d being Nat st d in dom fr holds

fr . d = (fp . d) * (x |^ (d -' 1)) ) & f . x = Sum fr )

thus for x being Element of INT ex fr being FinSequence of INT st

( len fr = len fp & ( for d being Nat st d in dom fr holds

fr . d = (fp . d) * (x |^ (d -' 1)) ) & f . x = Sum fr ) by A3; :: thesis: verum