let R be finite Approximation_Space; :: thesis: for X, Y being Subset of R st X <> {} holds
( kappa (X,Y) = ((CMap (kappa_1 R)) . (X,(Y `))) / (kappa_1 ((Y `),X)) & ((CMap (kappa_1 R)) . (X,(Y `))) / (kappa_1 ((Y `),X)) = ((CMap (kappa_2 R)) . (X,(Y `))) / (kappa_2 (([#] R),X)) )
let X, Y be Subset of R; :: thesis: ( X <> {} implies ( kappa (X,Y) = ((CMap (kappa_1 R)) . (X,(Y `))) / (kappa_1 ((Y `),X)) & ((CMap (kappa_1 R)) . (X,(Y `))) / (kappa_1 ((Y `),X)) = ((CMap (kappa_2 R)) . (X,(Y `))) / (kappa_2 (([#] R),X)) ) )
assume A0: X <> {} ; :: thesis: ( kappa (X,Y) = ((CMap (kappa_1 R)) . (X,(Y `))) / (kappa_1 ((Y `),X)) & ((CMap (kappa_1 R)) . (X,(Y `))) / (kappa_1 ((Y `),X)) = ((CMap (kappa_2 R)) . (X,(Y `))) / (kappa_2 (([#] R),X)) )
then kappa (X,Y) = ((CMap (kappa_1 R)) . (X,(Y `))) / (kappa_1 ((Y `),X)) by Lemma1;
hence ( kappa (X,Y) = ((CMap (kappa_1 R)) . (X,(Y `))) / (kappa_1 ((Y `),X)) & ((CMap (kappa_1 R)) . (X,(Y `))) / (kappa_1 ((Y `),X)) = ((CMap (kappa_2 R)) . (X,(Y `))) / (kappa_2 (([#] R),X)) ) by A0, Lemma2; :: thesis: verum