theorem Th16: :: MEASURE1:16

for A being set ex F being sequence of {A} st
for n being Element of NAT holds F . n = A