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 misses A /\ B by XBOOLE_0:def 7;
then (B \ A) --> 0 tolerates (A /\ B) --> 1 by FUNCOP_1:87;
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 Lm10; :: thesis: verum