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
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 A2: ( n in dom (R (#) f) & (R (#) f) . n = G ) ; :: thesis: d in dom G
set m = min (len R),(len f);
A3: ( min (len R),(len f) <= len R & min (len R),(len f) <= len f ) by XXREAL_0:17;
len (R (#) f) = min (len R),(len f) by Def7;
then A4: ( 1 <= n & n <= min (len R),(len f) ) by A2, FINSEQ_3:27;
then ( n <= len R & n <= len f ) by A3, XXREAL_0:2;
then A5: ( n in dom R & n in dom f ) by A4, FINSEQ_3:27;
reconsider r = R . n as Real ;
reconsider F = f . n as Element of PFuncs D,REAL by A5, FINSEQ_2:13;
A6: G = r (#) F by A2, Def7;
d in dom F by A1, A5, Def9;
hence d in dom G by A6, VALUED_1:def 5; :: thesis: verum