let A, B be set ; :: thesis: chi (A,B) = ((B \ A) --> 0) \/ ((A /\ B) --> 1)
set f = (B \ A) --> 0;
set g = (A /\ B) --> 1;
(B \ A) /\ (A /\ B) = {} ;
then (B \ A) --> 0 tolerates (A /\ B) --> 1 by FUNCOP_1:87, XBOOLE_0:def 7;
then ((B \ A) --> 0) +* ((A /\ B) --> 1) = ((B \ A) --> 0) \/ ((A /\ B) --> 1) by FUNCT_4:30;
hence chi (A,B) = ((B \ A) --> 0) \/ ((A /\ B) --> 1) by Lm39; :: thesis: verum