theorem :: RFUNCT_1:63

for X being set
for C being non empty set
for c being Element of C holds
( c in X iff (chi (X,C)) . c = 1 ) by Th61;