let f1, f2 be Function of INT,INT; :: 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)) ) & f1 . x = Sum fr ) ) & ( 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)) ) & f2 . x = Sum fr ) ) implies f1 = f2 )
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: f1 = f2
for x being Element of INT holds f1 . x = f2 . x

proof

let x be Element of INT ; :: thesis: f1 . x = f2 . x
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

proof

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

end;

hence f1 . x = f2 . x by A8, A11, A12, FINSEQ_1:13; :: thesis: verum

end;

hence f1 = f2 by FUNCT_2:63; :: thesis: verum