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) ;
A1:
( (A /\ B) \/ (B \ A) = B & dom (chi (A,B)) = BB )
by XBOOLE_1:51, FUNCT_3:def 3;
A2:
( B /\ OO = OO & (B \ A) /\ (A /\ B) = {} & B /\ ZZ = ZZ )
;
A3:
( ((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;
A4:
( (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 FUNCOP_1:12, A2;
then
( dom ((B --> 0) | (A /\ B)) = OOO & dom (((A /\ B) --> 1) | (A /\ B)) = A /\ B )
;
then A5:
((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 FUNCT_4:70, A1
.=
(((B --> 0) +* ((A /\ B) --> 1)) | (B \ A)) +* ((chi (A,B)) | (A /\ B))
by Lm38
.=
(((B /\ (B \ A)) --> 0) +* {}) +* (((A /\ B) --> 1) | (A /\ B))
by A3, Lm38, A4, A5
.=
((B \ A) --> 0) +* ((A /\ B) --> 1)
; verum