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