let R be finite Approximation_Space; for X, Y being Subset of R st X <> {} holds
kappa (X,Y) = ((CMap (kappa_2 R)) . (X,(Y `))) / (kappa_2 (([#] R),X))
let X, Y be Subset of R; ( X <> {} implies kappa (X,Y) = ((CMap (kappa_2 R)) . (X,(Y `))) / (kappa_2 (([#] R),X)) )
assume a1:
X <> {}
; kappa (X,Y) = ((CMap (kappa_2 R)) . (X,(Y `))) / (kappa_2 (([#] R),X))
VV:
X /\ ((Y `) `) = X \ (Y `)
by SUBSET_1:13;
((CMap (kappa_2 R)) . (X,(Y `))) / (kappa_2 (([#] R),X)) =
((card (X \ (Y `))) / (card ([#] R))) / ((card ((([#] R) `) \/ X)) / (card ([#] R)))
by PropEx31
.=
(card (X \ (Y `))) / (card (((({} R) `) `) \/ X))
by XCMPLX_1:55
.=
kappa (X,Y)
by ROUGHIF1:def 1, a1, VV
;
hence
kappa (X,Y) = ((CMap (kappa_2 R)) . (X,(Y `))) / (kappa_2 (([#] R),X))
; verum