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: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 ; :: 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 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 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; :: 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