let R be finite Approximation_Space; :: thesis: for X, Y being Subset of R holds kappa (([#] R),((X `) \/ Y)) = (kappa (([#] R),(X `))) + (kappa (([#] R),(X /\ Y)))
let X, Y be Subset of R; :: thesis: kappa (([#] R),((X `) \/ Y)) = (kappa (([#] R),(X `))) + (kappa (([#] R),(X /\ Y)))
a0: X ` misses X by XBOOLE_1:85;
(X `) \/ Y = ([#] R) /\ ((X `) \/ Y)
.= ((X `) \/ X) /\ ((X `) \/ Y) by PRE_TOPC:2
.= (X `) \/ (X /\ Y) by XBOOLE_1:24 ;
then A1: card ((X `) \/ Y) = (card (X `)) + (card (X /\ Y)) by a0, CARD_2:40, XBOOLE_1:74;
kappa (([#] R),((X `) \/ Y)) = (card (([#] R) /\ ((X `) \/ Y))) / (card ([#] R)) by KappaDef
.= ((card (([#] R) /\ (X `))) / (card ([#] R))) + ((card (X /\ Y)) / (card ([#] R))) by XCMPLX_1:62, A1
.= (kappa (([#] R),(X `))) + ((card ((X /\ Y) /\ ([#] R))) / (card ([#] R))) by KappaDef
.= (kappa (([#] R),(X `))) + (kappa (([#] R),(X /\ Y))) by KappaDef ;
hence kappa (([#] R),((X `) \/ Y)) = (kappa (([#] R),(X `))) + (kappa (([#] R),(X /\ Y))) ; :: thesis: verum