let p1, p2 be FinSequence of REAL ; :: thesis: ( len p1 = len f & ( for n being Element of NAT
for G being Element of PFuncs D,REAL st n in dom p1 & f . n = G holds
p1 . n = G . d ) & len p2 = len f & ( for n being Element of NAT
for G being Element of PFuncs D,REAL st n in dom p2 & f . n = G holds
p2 . n = G . d ) implies p1 = p2 )
assume that
A4: ( len p1 = len f & ( for n being Element of NAT
for G being Element of PFuncs D,REAL st n in dom p1 & f . n = G holds
p1 . n = G . d ) ) and
A5: ( len p2 = len f & ( for n being Element of NAT
for G being Element of PFuncs D,REAL st n in dom p2 & f . n = G holds
p2 . n = G . d ) ) ; :: thesis: p1 = p2
A6: ( dom p1 = Seg (len p1) & dom p2 = Seg (len p2) ) by FINSEQ_1:def 3;

now

let n be Nat; :: thesis: ( n in dom p1 implies p1 . n = p2 . n )
assume A7: n in dom p1 ; :: thesis: p1 . n = p2 . n
then n in dom f by A4, A6, FINSEQ_1:def 3;
then reconsider G = f . n as Element of PFuncs D,REAL by FINSEQ_2:13;
( p1 . n = G . d & p2 . n = G . d ) by A4, A5, A6, A7;
hence p1 . n = p2 . n ; :: thesis: verum

end;

hence p1 = p2 by A4, A5, FINSEQ_2:10; :: thesis: verum