for X being non empty set
for A being set
for S being SigmaField of X
for F being Finite_Sep_Sequence of S
for G being FinSequence of S st dom G = dom F & ( for i being Nat st i in dom G holds
G . i = A /\ (F . i) ) holds
G is Finite_Sep_Sequence of S