let X, Y be set ; :: thesis: chi (X,Y) is Function of Y,REAL
( ( {0,1} = {} implies X = {} ) & {0,1} c= REAL ) by INT_1:3, NUMBERS:19;
hence chi (X,Y) is Function of Y,REAL by FUNCT_2:7; :: thesis: verum