let A, B be set ; ( (chi (A,B)) " {0} = B \ A & (chi (A,B)) " {1} = A /\ B )
set f = (B \ A) --> 0;
set g = (A /\ B) --> 1;
set IT = chi (A,B);
B0:
( 0 in {0} & 1 in {1} & not 1 in {0} & not 0 in {1} )
by TARSKI:def 1;
B2:
( ((B \ A) --> 0) " {1} = {} & ((A /\ B) --> 1) " {0} = {} )
by B0, FUNCOP_1:16;
thus (chi (A,B)) " {0} =
(((B \ A) --> 0) \/ ((A /\ B) --> 1)) " {0}
by Lm29
.=
(((B \ A) --> 0) " {0}) \/ (((A /\ B) --> 1) " {0})
by Th23
.=
B \ A
by B0, B2, FUNCOP_1:14
; (chi (A,B)) " {1} = A /\ B
thus (chi (A,B)) " {1} =
(((B \ A) --> 0) \/ ((A /\ B) --> 1)) " {1}
by Lm29
.=
(((B \ A) --> 0) " {1}) \/ (((A /\ B) --> 1) " {1})
by Th23
.=
A /\ B
by B0, B2, FUNCOP_1:14
; verum