set m = min ((len R),(len f));
let p1, p2 be FinSequence of PFuncs (D,REAL); :: thesis: ( len p1 = min ((len R),(len f)) & ( for n being Nat st n in dom p1 holds
for F being PartFunc of D,REAL
for r being Real st r = R . n & F = f . n holds
p1 . n = r (#) F ) & len p2 = min ((len R),(len f)) & ( for n being Nat st n in dom p2 holds
for F being PartFunc of D,REAL
for r being Real st r = R . n & F = f . n holds
p2 . n = r (#) F ) implies p1 = p2 )
assume that
A6: len p1 = min ((len R),(len f)) and
A7: for n being Nat st n in dom p1 holds
for F being PartFunc of D,REAL
for r being Real st r = R . n & F = f . n holds
p1 . n = r (#) F and
A8: len p2 = min ((len R),(len f)) and
A9: for n being Nat st n in dom p2 holds
for F being PartFunc of D,REAL
for r being Real st r = R . n & F = f . n holds
p2 . n = r (#) F ; :: thesis: p1 = p2
A10: dom p1 = Seg (min ((len R),(len f))) by A6, FINSEQ_1:def 3;
A11: ( dom p1 = Seg (len p1) & dom p2 = Seg (len p2) ) by FINSEQ_1:def 3;
A12: min ((len R),(len f)) <= len f by XXREAL_0:17;

now :: thesis: for n being Nat st n in dom p1 holds
p1 . n = p2 . n

let n be Nat; :: thesis: ( n in dom p1 implies p1 . n = p2 . n )
reconsider r = R . n as Real ;
assume A13: n in dom p1 ; :: thesis: p1 . n = p2 . n
then n <= min ((len R),(len f)) by A10, FINSEQ_1:1;
then A14: n <= len f by A12, XXREAL_0:2;
1 <= n by A10, A13, FINSEQ_1:1;
then n in dom f by A14, FINSEQ_3:25;
then reconsider F = f . n as Element of PFuncs (D,REAL) by FINSEQ_2:11;
p1 . n = r (#) F by A7, A13;
hence p1 . n = p2 . n by A6, A8, A9, A11, A13; :: thesis: verum

end;

hence p1 = p2 by A6, A8, FINSEQ_2:9; :: thesis: verum