let A be finite Approximation_Space; :: thesis: for X, Y being Subset of A
for x being Element of A st X misses Y holds
(MemberFunc (X \/ Y),A) . x = ((MemberFunc X,A) . x) + ((MemberFunc Y,A) . x)
let X, Y be Subset of A; :: thesis: for x being Element of A st X misses Y holds
(MemberFunc (X \/ Y),A) . x = ((MemberFunc X,A) . x) + ((MemberFunc Y,A) . x)
let x be Element of A; :: thesis: ( X misses Y implies (MemberFunc (X \/ Y),A) . x = ((MemberFunc X,A) . x) + ((MemberFunc Y,A) . x) )
assume A1: X misses Y ; :: thesis: (MemberFunc (X \/ Y),A) . x = ((MemberFunc X,A) . x) + ((MemberFunc Y,A) . x)
card ((X \/ Y) /\ (Class the InternalRel of A,x)) = card ((X /\ (Class the InternalRel of A,x)) \/ (Y /\ (Class the InternalRel of A,x))) by XBOOLE_1:23
.= (card (X /\ (Class the InternalRel of A,x))) + (card (Y /\ (Class the InternalRel of A,x))) by A1, CARD_2:53, XBOOLE_1:76 ;
then (MemberFunc (X \/ Y),A) . x = ((card (X /\ (Class the InternalRel of A,x))) + (card (Y /\ (Class the InternalRel of A,x)))) / (card (Class the InternalRel of A,x)) by Def9
.= ((card (X /\ (Class the InternalRel of A,x))) / (card (Class the InternalRel of A,x))) + ((card (Y /\ (Class the InternalRel of A,x))) / (card (Class the InternalRel of A,x))) by XCMPLX_1:63
.= ((MemberFunc X,A) . x) + ((card (Y /\ (Class the InternalRel of A,x))) / (card (Class the InternalRel of A,x))) by Def9
.= ((MemberFunc X,A) . x) + ((MemberFunc Y,A) . x) by Def9 ;
hence (MemberFunc (X \/ Y),A) . x = ((MemberFunc X,A) . x) + ((MemberFunc Y,A) . x) ; :: thesis: verum