defpred S₁[ 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₁[x,y]

proof

let x be Element of INT ; :: thesis: ex y being Element of INT st S₁[x,y]
deffunc H₁( 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₁(d) ) ) from FINSEQ_1:sch 2();
for d being Nat st d in dom fr holds
fr . d in INT

proof

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;

then reconsider fr = fr as FinSequence of INT by FINSEQ_2:12;
take Sum fr ; :: thesis: S₁[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;

consider f being Function of INT,INT such that
A3: for x being Element of INT holds S₁[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