let A, B be set ; :: thesis: chi (A,B) = (B --> 0) +* ((A /\ B) --> 1)
set f = B --> 0;
set g = (A /\ B) --> 1;
set IT = (B --> 0) +* ((A /\ B) --> 1);
B1: ( dom (B --> 0) = B & dom ((A /\ B) --> 1) = A /\ B & dom ((B --> 0) +* ((A /\ B) --> 1)) = (dom (B --> 0)) \/ (dom ((A /\ B) --> 1)) ) by FUNCOP_1:13, FUNCT_4:def 1;
B0: dom ((B --> 0) +* ((A /\ B) --> 1)) = B by B1, XBOOLE_1:22;

now

let x be set ; :: thesis: ( x in B implies ( ( x in A implies ((B --> 0) +* ((A /\ B) --> 1)) . x = 1 ) & ( not x in A implies ((B --> 0) +* ((A /\ B) --> 1)) . x = {} ) ) )
assume Z0: x in B ; :: thesis: ( ( x in A implies ((B --> 0) +* ((A /\ B) --> 1)) . x = 1 ) & ( not x in A implies ((B --> 0) +* ((A /\ B) --> 1)) . x = {} ) )
then C0: ( x in B & x in dom ((B --> 0) +* ((A /\ B) --> 1)) & x in (dom (B --> 0)) \/ (dom ((A /\ B) --> 1)) ) by B1, XBOOLE_1:22;
thus ( x in A implies ((B --> 0) +* ((A /\ B) --> 1)) . x = 1 ) :: thesis: ( not x in A implies ((B --> 0) +* ((A /\ B) --> 1)) . x = {} )

proof

assume Z1: x in A ; :: thesis: ((B --> 0) +* ((A /\ B) --> 1)) . x = 1
then D0: x in A /\ B by Z0, XBOOLE_0:def 4;
x in dom ((A /\ B) --> 1) by Z1, Z0, B1, XBOOLE_0:def 4;
then ((B --> 0) +* ((A /\ B) --> 1)) . x = ((A /\ B) --> 1) . x by C0, FUNCT_4:def 1
.= 1 by D0, FUNCOP_1:7 ;
hence ((B --> 0) +* ((A /\ B) --> 1)) . x = 1 ; :: thesis: verum

end;

thus ( not x in A implies ((B --> 0) +* ((A /\ B) --> 1)) . x = {} ) :: thesis: verum

proof

assume not x in A ; :: thesis: ((B --> 0) +* ((A /\ B) --> 1)) . x = {}
then not x in A /\ B ;
then not x in dom ((A /\ B) --> 1) ;
then ((B --> 0) +* ((A /\ B) --> 1)) . x = (B --> 0) . x by C0, FUNCT_4:def 1
.= 0 by Z0, FUNCOP_1:7 ;
hence ((B --> 0) +* ((A /\ B) --> 1)) . x = {} ; :: thesis: verum

end;

end;

hence chi (A,B) = (B --> 0) +* ((A /\ B) --> 1) by B0, FUNCT_3:def 3; :: thesis: verum