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 n be Nat; :: according to RFUNCT_3:def 9 :: thesis: ( n in dom (R (#) f) implies d in dom ((R (#) f) . n) )
assume A2: n in dom (R (#) f) ; :: thesis: d in dom ((R (#) f) . n)
set G = (R (#) f) . n;
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:25, XXREAL_0:17;
then A3: n <= len f by XXREAL_0:2;
1 <= n by A2, FINSEQ_3:25;
then A4: n in dom f by A3, FINSEQ_3:25;
then reconsider F = f . n as Element of PFuncs (D,REAL) by FINSEQ_2:11;
A5: d in dom F by A1, A4;
reconsider r = R . n as Real ;
(R (#) f) . n = r (#) F by A2, Def7;
hence d in dom ((R (#) f) . n) by A5, VALUED_1:def 5; :: thesis: verum