theorem :: YELLOW15:13

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