let D be non empty set ; for f being FinSequence
for d being Element of D holds d is_common_for_dom CHI (f,D)
let f be FinSequence; for d being Element of D holds d is_common_for_dom CHI (f,D)
let d be Element of D; d is_common_for_dom CHI (f,D)
let n be Nat; RFUNCT_3:def 9 ( n in dom (CHI (f,D)) implies d in dom ((CHI (f,D)) . n) )
assume
n in dom (CHI (f,D))
; 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)
; verum