theorem :: MEASUR11:6

for X being non empty set
for S being non empty Subset-Family of X
for f being FinSequence of S
for F being FinSequence of PFuncs (X,ExtREAL) st dom f = dom F & f is disjoint_valued & ( for n being Nat st n in dom F holds
F . n = chi ((f . n),X) ) holds
for x being Element of X holds (chi ((Union f),X)) . x = Sum (F # x)