theorem :: YELLOW15:9

for X being set
for x being Subset of X
for q being FinSequence of BOOLEAN holds len (MergeSequence (<*x*>,q)) = 1