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:40, 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:62
.= ((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