let X, Y be set ; for C being non empty set st X misses Y holds
(chi (X,C)) + (chi (Y,C)) = chi ((X \/ Y),C)
let C be non empty set ; ( X misses Y implies (chi (X,C)) + (chi (Y,C)) = chi ((X \/ Y),C) )
assume A1:
X /\ Y = {}
; XBOOLE_0:def 7 (chi (X,C)) + (chi (Y,C)) = chi ((X \/ Y),C)
A2:
now for c being Element of C st c in dom ((chi (X,C)) + (chi (Y,C))) holds
((chi (X,C)) + (chi (Y,C))) . c = (chi ((X \/ Y),C)) . clet c be
Element of
C;
( c in dom ((chi (X,C)) + (chi (Y,C))) implies ((chi (X,C)) + (chi (Y,C))) . c = (chi ((X \/ Y),C)) . c )assume A3:
c in dom ((chi (X,C)) + (chi (Y,C)))
;
((chi (X,C)) + (chi (Y,C))) . c = (chi ((X \/ Y),C)) . cnow ((chi (X,C)) . c) + ((chi (Y,C)) . c) = (chi ((X \/ Y),C)) . cper cases
( c in X or not c in X )
;
suppose A4:
c in X
;
((chi (X,C)) . c) + ((chi (Y,C)) . c) = (chi ((X \/ Y),C)) . cthen
not
c in Y
by A1, XBOOLE_0:def 4;
then A5:
(chi (Y,C)) . c = 0
by Th61;
A6:
c in X \/ Y
by A4, XBOOLE_0:def 3;
(chi (X,C)) . c = 1
by A4, Th61;
hence
((chi (X,C)) . c) + ((chi (Y,C)) . c) = (chi ((X \/ Y),C)) . c
by A5, A6, Th61;
verum end; end; end; hence
((chi (X,C)) + (chi (Y,C))) . c = (chi ((X \/ Y),C)) . c
by A3, VALUED_1:def 1;
verum end;
dom ((chi (X,C)) + (chi (Y,C))) =
(dom (chi (X,C))) /\ (dom (chi (Y,C)))
by VALUED_1:def 1
.=
C /\ (dom (chi (Y,C)))
by Th61
.=
C /\ C
by Th61
.=
dom (chi ((X \/ Y),C))
by Th61
;
hence
(chi (X,C)) + (chi (Y,C)) = chi ((X \/ Y),C)
by A2, PARTFUN1:5; verum