let f1, f2 be Function of INT,INT; :: thesis:
assume that
A4: for x being Element of INT ex fr1 being FinSequence of INT st
( len fr1 = len fp & ( for d being Nat st d in dom fr1 holds
fr1 . d = (fp . d) * (x |^ (d -' 1)) ) & f1 . x = Sum fr1 ) and
A5: for x being Element of INT ex fr2 being FinSequence of INT st
( len fr2 = len fp & ( for d being Nat st d in dom fr2 holds
fr2 . d = (fp . d) * (x |^ (d -' 1)) ) & f2 . x = Sum fr2 ) ; :: thesis:
for x being Element of INT holds f1 . x = f2 . x

let x be Element of INT ; :: thesis:
consider fr1 being FinSequence of INT such that
A6: len fr1 = len fp and
A7: for d being Nat st d in dom fr1 holds
fr1 . d = (fp . d) * (x |^ (d -' 1)) and
A8: f1 . x = Sum fr1 by A4;
consider fr2 being FinSequence of INT such that
A9: len fr2 = len fp and
A10: for d being Nat st d in dom fr2 holds
fr2 . d = (fp . d) * (x |^ (d -' 1)) and
A11: f2 . x = Sum fr2 by A5;
A12: dom fr1 = dom fr2 by A6, A9, FINSEQ_3:29;
for d being Nat st d in dom fr1 holds
fr1 . d = fr2 . d

let d be Nat; :: thesis:
assume A13: d in dom fr1 ; :: thesis:
hence fr2 . d = (fp . d) * (x |^ (d -' 1)) by A10, A12
.= fr1 . d by A7, A13 ;
:: thesis:

end;

end;