theorem Th16: :: SETLIM_1:16

for X being set
for B being SetSequence of X
for f being Function st dom f = NAT & ( for n being Nat holds f . n = union { (B . k) where k is Nat : n <= k } ) holds
f is sequence of (bool X)