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

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