set m = min ((len R),(len f));
let p1, p2 be FinSequence of PFuncs (D,REAL); ( 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
; 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 for n being Nat st n in dom p1 holds
p1 . n = p2 . nlet n be
Nat;
( n in dom p1 implies p1 . n = p2 . n )reconsider r =
R . n as
Real ;
assume A13:
n in dom p1
;
p1 . n = p2 . nthen
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;
verum end;
hence
p1 = p2
by A6, A8, FINSEQ_2:9; verum