defpred S1[ Nat, set ] means for F being PartFunc of D,REAL
for r being Real st r = R . $1 & F = f . $1 holds
$2 = r (#) F;
set m = min ((len R),(len f));
A1:
min ((len R),(len f)) <= len f
by XXREAL_0:17;
A2:
for n being Nat st n in Seg (min ((len R),(len f))) holds
ex x being Element of PFuncs (D,REAL) st S1[n,x]
proof
let n be
Nat;
( n in Seg (min ((len R),(len f))) implies ex x being Element of PFuncs (D,REAL) st S1[n,x] )
reconsider r =
R . n as
Real ;
assume A3:
n in Seg (min ((len R),(len f)))
;
ex x being Element of PFuncs (D,REAL) st S1[n,x]
then
n <= min (
(len R),
(len f))
by FINSEQ_1:1;
then A4:
n <= len f
by A1, XXREAL_0:2;
1
<= n
by A3, FINSEQ_1:1;
then
n in dom f
by A4, FINSEQ_3:25;
then reconsider F =
f . n as
Element of
PFuncs (
D,
REAL)
by FINSEQ_2:11;
reconsider a =
r (#) F as
Element of
PFuncs (
D,
REAL) ;
take
a
;
S1[n,a]
thus
S1[
n,
a]
;
verum
end;
consider p being FinSequence of PFuncs (D,REAL) such that
A5:
( dom p = Seg (min ((len R),(len f))) & ( for n being Nat st n in Seg (min ((len R),(len f))) holds
S1[n,p . n] ) )
from FINSEQ_1:sch 5(A2);
take
p
; ( len p = min ((len R),(len f)) & ( for n being Nat st n in dom p holds
for F being PartFunc of D,REAL
for r being Real st r = R . n & F = f . n holds
p . n = r (#) F ) )
thus
len p = min ((len R),(len f))
by A5, FINSEQ_1:def 3; for n being Nat st n in dom p holds
for F being PartFunc of D,REAL
for r being Real st r = R . n & F = f . n holds
p . n = r (#) F
let n be Nat; ( n in dom p implies for F being PartFunc of D,REAL
for r being Real st r = R . n & F = f . n holds
p . n = r (#) F )
assume
n in dom p
; for F being PartFunc of D,REAL
for r being Real st r = R . n & F = f . n holds
p . n = r (#) F
hence
for F being PartFunc of D,REAL
for r being Real st r = R . n & F = f . n holds
p . n = r (#) F
by A5; verum