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);
A1: ( dom (B --> 0) = B & dom ((A /\ B) --> 1) = A /\ B & dom ((B --> 0) +* ((A /\ B) --> 1)) = (dom (B --> 0)) \/ (dom ((A /\ B) --> 1)) ) by FUNCT_4:def 1;

now :: thesis: for x being object st x in B holds
( ( x in A implies ((B --> 0) +* ((A /\ B) --> 1)) . x = 1 ) & ( not x in A implies ((B --> 0) +* ((A /\ B) --> 1)) . x = {} ) )

let x be object ; :: 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 A2: 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 A3: ( x in B & x in dom ((B --> 0) +* ((A /\ B) --> 1)) & x in (dom (B --> 0)) \/ (dom ((A /\ B) --> 1)) ) by XBOOLE_1:22, A1;
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 A4: x in A ; :: thesis: ((B --> 0) +* ((A /\ B) --> 1)) . x = 1
then A5: x in A /\ B by A2, XBOOLE_0:def 4;
x in dom ((A /\ B) --> 1) by A4, A2, XBOOLE_0:def 4;
then ((B --> 0) +* ((A /\ B) --> 1)) . x = ((A /\ B) --> 1) . x by A3, FUNCT_4:def 1
.= 1 by FUNCOP_1:7, A5 ;
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 A3, FUNCT_4:def 1
.= 0 by FUNCOP_1:7, A2 ;
hence ((B --> 0) +* ((A /\ B) --> 1)) . x = {} ; :: thesis: verum

end;

end;

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