defpred S1[ 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 S1[x,y]
proof
let x be Element of INT ; :: thesis: ex y being Element of INT st S1[x,y]
deffunc H1( 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 = H1(d) ) ) from 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: S1[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 S1[x,f . x] from 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