let p1, p2 be FinSequence of PFuncs D,REAL ; :: thesis: ( len p1 = min (len R),(len f) & ( for n being Element of 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 Element of 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 )
set m = min (len R),(len f);
assume that
A5: len p1 = min (len R),(len f) and
A6: for n being Element of 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
A7: len p2 = min (len R),(len f) and
A8: for n being Element of 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
A9: ( min (len R),(len f) <= len R & min (len R),(len f) <= len f ) by XXREAL_0:17;
A10: ( dom p1 = Seg (len p1) & dom p2 = Seg (len p2) ) by FINSEQ_1:def 3;
X: dom p1 = Seg (min (len R),(len f)) by A5, FINSEQ_1:def 3;

now

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

end;

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