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 :: 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
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 :: thesis: ((chi (X,C)) . c) + ((chi (Y,C)) . c) = (chi ((X \/ Y),C)) . c
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 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;
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;
now :: thesis: ((chi (X,C)) . c) + ((chi (Y,C)) . c) = (chi ((X \/ Y),C)) . c
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, Th61;
hence ((chi (X,C)) . c) + ((chi (Y,C)) . c) = (chi ((X \/ Y),C)) . c by A8, A10, Th61; :: 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, Th61;
hence ((chi (X,C)) . c) + ((chi (Y,C)) . c) = (chi ((X \/ Y),C)) . c by A8, A12, Th61; :: 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 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