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);
A1:
( 0 in {0} & 1 in {1} & not 1 in {0} & not 0 in {1} )
by TARSKI:def 1;
A2:
( ((B \ A) --> 0) " {1} = {} & ((A /\ B) --> 1) " {0} = {} )
by A1, FUNCOP_1:16;
thus (chi (A,B)) " {0} =
(((B \ A) --> 0) \/ ((A /\ B) --> 1)) " {0}
by Lm40
.=
(((B \ A) --> 0) " {0}) \/ (((A /\ B) --> 1) " {0})
by Th23
.=
B \ A
by A1, FUNCOP_1:14, A2
; (chi (A,B)) " {1} = A /\ B
thus (chi (A,B)) " {1} =
(((B \ A) --> 0) \/ ((A /\ B) --> 1)) " {1}
by Lm40
.=
(((B \ A) --> 0) " {1}) \/ (((A /\ B) --> 1) " {1})
by Th23
.=
A /\ B
by A1, FUNCOP_1:14, A2
; verum