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

( 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

hence
f1 = f2
by FUNCT_2:63; :: thesis: verum
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

end;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

hence
f1 . x = f2 . x
by A8, A11, A12, FINSEQ_1:13; :: thesis: verum
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;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