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