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

A2: now

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

now

per cases ( c in X or not c in X ) ;

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 Th77;
A6: c in X \/ Y by A4, XBOOLE_0:def 3;
(chi X,C) . c = 1 by A4, Th77;
hence ((chi X,C) . c) + ((chi Y,C) . c) = (chi (X \/ Y),C) . c by A5, A6, Th77; :: thesis: verum

end;

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 Th77;

now

per cases ( c in Y or not c in Y ) ;

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

then A10: c in X \/ Y by XBOOLE_0:def 3;
(chi Y,C) . c = 1 by A9, Th77;
hence ((chi X,C) . c) + ((chi Y,C) . c) = (chi (X \/ Y),C) . c by A8, A10, Th77; :: thesis: verum

end;

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

then A12: not c in X \/ Y by A7, XBOOLE_0:def 3;
(chi Y,C) . c = 0 by A11, Th77;
hence ((chi X,C) . c) + ((chi Y,C) . c) = (chi (X \/ Y),C) . c by A8, A12, Th77; :: thesis: verum

end;

end;

end;

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

end;

end;

end;

hence ((chi X,C) + (chi Y,C)) . c = (chi (X \/ Y),C) . c by A3, VALUED_1:def 1; :: thesis: 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 Th77
.= C /\ C by Th77
.= dom (chi (X \/ Y),C) by Th77 ;
hence (chi X,C) + (chi Y,C) = chi (X \/ Y),C by A2, PARTFUN1:34; :: thesis: verum