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 n be Nat; :: according to RFUNCT_3:def 9 :: thesis: ( n in dom (CHI (f,D)) implies d in dom ((CHI (f,D)) . n) )
assume n in dom (CHI (f,D)) ; :: thesis: d in dom ((CHI (f,D)) . n)
then (CHI (f,D)) . n = chi ((f . n),D) by Def6;
then dom ((CHI (f,D)) . n) = D by RFUNCT_1:61;
hence d in dom ((CHI (f,D)) . n) ; :: thesis: verum