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

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 A5: (chi X,C) . c = 1 by Th77;
not c in Y by A1, A4, XBOOLE_0:def 4;
then A6: (chi Y,C) . c = 0 by Th77;
c in X \/ Y by A4, XBOOLE_0:def 3;
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: (chi Y,C) . c = 1 by Th77;
c in X \/ Y by A9, XBOOLE_0:def 3;
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: (chi Y,C) . c = 0 by Th77;
not c in X \/ Y by A7, A11, XBOOLE_0:def 3;
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;

hence (chi X,C) + (chi Y,C) = chi (X \/ Y),C by A2, PARTFUN1:34; :: thesis: verum