defpred S₁[ 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 S₁[n,x]

proof

let n be Nat; :: thesis: ( n in Seg (min (len R),(len f)) implies ex x being Element of PFuncs D,REAL st S₁[n,x] )
reconsider r = R . n as Real ;
assume A3: n in Seg (min (len R),(len f)) ; :: thesis: ex x being Element of PFuncs D,REAL st S₁[n,x]
then n <= min (len R),(len f) by FINSEQ_1:3;
then A4: n <= len f by A1, XXREAL_0:2;
1 <= n by A3, FINSEQ_1:3;
then n in dom f by A4, FINSEQ_3:27;
then reconsider F = f . n as Element of PFuncs D,REAL by FINSEQ_2:13;
reconsider a = r (#) F as Element of PFuncs D,REAL ;
take a ; :: thesis: S₁[n,a]
thus S₁[n,a] ; :: thesis: 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
S₁[n,p . n] ) ) from FINSEQ_1:sch 5(A2);
take p ; :: thesis: ( len p = min (len R),(len f) & ( for n being Element of 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; :: thesis: for n being Element of 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 Element of NAT ; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum