let X, Y be set ; :: thesis: 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 ; :: thesis: ( X misses Y implies (chi (X,C)) + (chi (Y,C)) = chi ((X \/ Y),C) )

assume A1: X /\ Y = {} ; :: according to XBOOLE_0:def 7 :: thesis: (chi (X,C)) + (chi (Y,C)) = chi ((X \/ Y),C)

.= 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; :: thesis: verum

(chi (X,C)) + (chi (Y,C)) = chi ((X \/ Y),C)

let C be non empty set ; :: thesis: ( X misses Y implies (chi (X,C)) + (chi (Y,C)) = chi ((X \/ Y),C) )

assume A1: X /\ Y = {} ; :: according to XBOOLE_0:def 7 :: thesis: (chi (X,C)) + (chi (Y,C)) = chi ((X \/ Y),C)

A2: now :: thesis: 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)) . c

dom ((chi (X,C)) + (chi (Y,C))) =
(dom (chi (X,C))) /\ (dom (chi (Y,C)))
by VALUED_1:def 1
((chi (X,C)) + (chi (Y,C))) . c = (chi ((X \/ Y),C)) . c

let c be Element of C; :: thesis: ( 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))) ; :: thesis: ((chi (X,C)) + (chi (Y,C))) . c = (chi ((X \/ Y),C)) . c

end;assume A3: c in dom ((chi (X,C)) + (chi (Y,C))) ; :: thesis: ((chi (X,C)) + (chi (Y,C))) . c = (chi ((X \/ Y),C)) . c

now :: thesis: ((chi (X,C)) . c) + ((chi (Y,C)) . c) = (chi ((X \/ Y),C)) . cend;

hence
((chi (X,C)) + (chi (Y,C))) . c = (chi ((X \/ Y),C)) . c
by A3, VALUED_1:def 1; :: thesis: verumper cases
( c in X or not c in X )
;

end;

suppose A4:
c in X
; :: thesis: ((chi (X,C)) . c) + ((chi (Y,C)) . c) = (chi ((X \/ Y),C)) . c

then
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; :: thesis: verum

end;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; :: thesis: verum

suppose A7:
not c in X
; :: thesis: ((chi (X,C)) . c) + ((chi (Y,C)) . c) = (chi ((X \/ Y),C)) . c

then A8:
(chi (X,C)) . c = 0
by Th61;

end;now :: thesis: ((chi (X,C)) . c) + ((chi (Y,C)) . c) = (chi ((X \/ Y),C)) . cend;

hence
((chi (X,C)) . c) + ((chi (Y,C)) . c) = (chi ((X \/ Y),C)) . c
; :: thesis: verumper cases
( c in Y or not c in Y )
;

end;

.= 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; :: thesis: verum