for X being set
for S being SigmaField of X
for N being sequence of S
for A being Element of S ex F being sequence of S st
for n being Element of NAT holds F . n = A /\ (N . n)