theorem Th15: :: MEASURE3:15

for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for F being sequence of (COM (S,M)) ex G being sequence of S st
for n being Element of NAT holds G . n in MeasPart (F . n)