set m = min (len R),(len f);
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;
A1:
( min (len R),(len f) <= len R & 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;
:: thesis: ( n in Seg (min (len R),(len f)) implies ex x being Element of PFuncs D,REAL st S1[n,x] )
assume
n in Seg (min (len R),(len f))
;
:: thesis: ex x being Element of PFuncs D,REAL st S1[n,x]
then A3:
( 1
<= n &
n <= min (len R),
(len f) )
by FINSEQ_1:3;
then
(
n <= len R &
n <= len f )
by A1, XXREAL_0:2;
then
(
n in dom R &
n in dom f )
by A3, FINSEQ_3:27;
then reconsider F =
f . n as
Element of
PFuncs D,
REAL by FINSEQ_2:13;
reconsider r =
R . n as
Real ;
reconsider a =
r (#) F as
Element of
PFuncs D,
REAL ;
take
a
;
:: thesis: S1[n,a]
thus
S1[
n,
a]
;
:: thesis: verum
end;
consider p being FinSequence of PFuncs D,REAL such that
A4:
( 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
; :: 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 A4, 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 A4; :: thesis: verum