let X be set ; :: thesis: for q being FinSequence of BOOLEAN holds len (MergeSequence ((<*> (bool X)),q)) = 0
let q be FinSequence of BOOLEAN ; :: thesis: len (MergeSequence ((<*> (bool X)),q)) = 0
thus len (MergeSequence ((<*> (bool X)),q)) = len (<*> (bool X)) by Def1
.= 0 ; :: thesis: verum