theorem Th5: :: YELLOW15:8

for X being set
for q being FinSequence of BOOLEAN holds MergeSequence ((<*> (bool X)),q) = <*> (bool X)