theorem :: ROUGHS_1:55

for A being finite Approximation_Space
for x being Element of A
for X being disjoint_valued FinSequence of bool the carrier of A holds (MemberFunc ((Union X),A)) . x = Sum (FinSeqM (x,X))