let D be non empty set ; :: thesis: for d being Element of D
for f being FinSequence of PFuncs D,REAL
for R being FinSequence of REAL st d is_common_for_dom f holds
d is_common_for_dom R (#) f
let d be Element of D; :: thesis: for f being FinSequence of PFuncs D,REAL
for R being FinSequence of REAL st d is_common_for_dom f holds
d is_common_for_dom R (#) f
let f be FinSequence of PFuncs D,REAL ; :: thesis: for R being FinSequence of REAL st d is_common_for_dom f holds
d is_common_for_dom R (#) f
let R be FinSequence of REAL ; :: thesis: ( d is_common_for_dom f implies d is_common_for_dom R (#) f )
assume A1: d is_common_for_dom f ; :: thesis: d is_common_for_dom R (#) f
set m = min (len R),(len f);
let G be Element of PFuncs D,REAL ; :: according to RFUNCT_3:def 9 :: thesis: for n being Element of NAT st n in dom (R (#) f) & (R (#) f) . n = G holds
d in dom G
let n be Element of NAT ; :: thesis: ( n in dom (R (#) f) & (R (#) f) . n = G implies d in dom G )
assume that
A2: n in dom (R (#) f) and
A3: (R (#) f) . n = G ; :: thesis: d in dom G
len (R (#) f) = min (len R),(len f) by Def7;
then ( min (len R),(len f) <= len f & n <= min (len R),(len f) ) by A2, FINSEQ_3:27, XXREAL_0:17;
then A4: n <= len f by XXREAL_0:2;
1 <= n by A2, FINSEQ_3:27;
then A5: n in dom f by A4, FINSEQ_3:27;
then reconsider F = f . n as Element of PFuncs D,REAL by FINSEQ_2:13;
A6: d in dom F by A1, A5, Def9;
reconsider r = R . n as Real ;
G = r (#) F by A2, A3, Def7;
hence d in dom G by A6, VALUED_1:def 5; :: thesis: verum