let A, B be set ; :: thesis:
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;

let x be object ; :: thesis:
assume A2: x in B ; :: thesis:
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:

assume A4: x in A ; :: thesis:
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:

end;

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

assume not x in A ; :: thesis:
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:

end;