let A, B be set ; chi (A,B) = ((B \ A) --> 0) +* ((A /\ B) --> 1)
set Z = B \ A;
set O = A /\ B;
set f = B --> 0;
set g = (A /\ B) --> 1;
set IT = chi (A,B);
reconsider BB = B /\ B, OO = A /\ B, ZZ = B \ A as Subset of B ;
reconsider OOO = (A /\ B) /\ (A /\ B) as Subset of (A /\ B) ;
B4:
( (A /\ B) \/ (B \ A) = B & dom (chi (A,B)) = BB )
by FUNCT_3:def 3, XBOOLE_1:51;
B0:
( B /\ OO = OO & (B \ A) /\ (A /\ B) = {} & B /\ ZZ = ZZ )
;
B1:
( ((B --> 0) +* ((A /\ B) --> 1)) | (B \ A) = ((B --> 0) | (B \ A)) +* (((A /\ B) --> 1) | (B \ A)) & ((B --> 0) +* ((A /\ B) --> 1)) | (A /\ B) = ((B --> 0) | (A /\ B)) +* (((A /\ B) --> 1) | (A /\ B)) )
by FUNCT_4:71;
B2:
( (B --> 0) | (B \ A) = (B /\ (B \ A)) --> 0 & ((A /\ B) --> 1) | (B \ A) = {} --> 1 & (B --> 0) | (A /\ B) = OOO --> 0 & ((A /\ B) --> 1) | (A /\ B) = (A /\ B) --> 1 )
by B0, FUNCOP_1:12;
then
( dom ((B --> 0) | (A /\ B)) = OOO & dom (((A /\ B) --> 1) | (A /\ B)) = A /\ B )
by FUNCOP_1:13;
then B3:
((B --> 0) | (A /\ B)) +* (((A /\ B) --> 1) | (A /\ B)) = ((A /\ B) --> 1) | (A /\ B)
by FUNCT_4:19;
thus chi (A,B) =
((chi (A,B)) | (B \ A)) +* ((chi (A,B)) | (A /\ B))
by B4, FUNCT_4:70
.=
(((B --> 0) +* ((A /\ B) --> 1)) | (B \ A)) +* ((chi (A,B)) | (A /\ B))
by Lm4
.=
(((B /\ (B \ A)) --> 0) +* {}) +* (((A /\ B) --> 1) | (A /\ B))
by B1, Lm4, B2, B3
.=
((B \ A) --> 0) +* ((A /\ B) --> 1)
by FUNCT_4:21
; verum