let A be finite Approximation_Space; :: thesis: for X being Subset of A
for x being Element of A holds (MemberFunc (X ` ),A) . x = 1 - ((MemberFunc X,A) . x)
let X be Subset of A; :: thesis: for x being Element of A holds (MemberFunc (X ` ),A) . x = 1 - ((MemberFunc X,A) . x)
let x be Element of A; :: thesis: (MemberFunc (X ` ),A) . x = 1 - ((MemberFunc X,A) . x)
A1: ([#] A) /\ (Class the InternalRel of A,x) = Class the InternalRel of A,x by XBOOLE_1:28;
(MemberFunc (X ` ),A) . x = (card ((([#] A) \ X) /\ (Class the InternalRel of A,x))) / (card (Class the InternalRel of A,x)) by Def9
.= (card ((([#] A) /\ (Class the InternalRel of A,x)) \ (X /\ (Class the InternalRel of A,x)))) / (card (Class the InternalRel of A,x)) by XBOOLE_1:50
.= ((card (([#] A) /\ (Class the InternalRel of A,x))) - (card (X /\ (Class the InternalRel of A,x)))) / (card (Class the InternalRel of A,x)) by A1, CARD_2:63, XBOOLE_1:17
.= ((card (([#] A) /\ (Class the InternalRel of A,x))) / (card (Class the InternalRel of A,x))) - ((card (X /\ (Class the InternalRel of A,x))) / (card (Class the InternalRel of A,x))) by XCMPLX_1:121
.= ((card (Class the InternalRel of A,x)) / (card (Class the InternalRel of A,x))) - ((card (X /\ (Class the InternalRel of A,x))) / (card (Class the InternalRel of A,x))) by XBOOLE_1:28
.= 1 - ((card (X /\ (Class the InternalRel of A,x))) / (card (Class the InternalRel of A,x))) by XCMPLX_1:60
.= 1 - ((MemberFunc X,A) . x) by Def9 ;
hence (MemberFunc (X ` ),A) . x = 1 - ((MemberFunc X,A) . x) ; :: thesis: verum