theorem :: YELLOW15:10

for X being set
for x being Subset of X
for q being FinSequence of BOOLEAN holds
( ( q . 1 = TRUE implies (MergeSequence (<*x*>,q)) . 1 = x ) & ( q . 1 = FALSE implies (MergeSequence (<*x*>,q)) . 1 = X \ x ) )