:: deftheorem Def6 defines CHI RFUNCT_3:def 6 :
for D being non empty set
for f being FinSequence
for b₃ being FinSequence of PFuncs (D,REAL) holds
( b₃ = CHI (f,D) iff ( len b₃ = len f & ( for n being Nat st n in dom b₃ holds
b₃ . n = chi ((f . n),D) ) ) );