let D be non empty set ; :: thesis: for f being FinSequence
for d being Element of D holds d is_common_for_dom CHI f,D
let f be FinSequence; :: thesis: for d being Element of D holds d is_common_for_dom CHI f,D
let d be Element of D; :: thesis: d is_common_for_dom CHI f,D
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 (CHI f,D) & (CHI f,D) . n = G holds
d in dom G
let n be Element of NAT ; :: thesis: ( n in dom (CHI f,D) & (CHI f,D) . n = G implies d in dom G )
assume ( n in dom (CHI f,D) & (CHI f,D) . n = G ) ; :: thesis: d in dom G
then G = chi (f . n),D by Def6;
then dom G = D by RFUNCT_1:77;
hence d in dom G ; :: thesis: verum