theorem :: FUNCT_3:40
for X being set
for f being Function of X,{0,1} holds f = chi ((f " {1}),X)