let X be set ; :: thesis: for x, y being Subset of X

for q being FinSequence of BOOLEAN holds len (MergeSequence (<*x,y*>,q)) = 2

let x, y be Subset of X; :: thesis: for q being FinSequence of BOOLEAN holds len (MergeSequence (<*x,y*>,q)) = 2

let q be FinSequence of BOOLEAN ; :: thesis: len (MergeSequence (<*x,y*>,q)) = 2

thus len (MergeSequence (<*x,y*>,q)) = len <*x,y*> by Def1

.= 2 by FINSEQ_1:44 ; :: thesis: verum

for q being FinSequence of BOOLEAN holds len (MergeSequence (<*x,y*>,q)) = 2

let x, y be Subset of X; :: thesis: for q being FinSequence of BOOLEAN holds len (MergeSequence (<*x,y*>,q)) = 2

let q be FinSequence of BOOLEAN ; :: thesis: len (MergeSequence (<*x,y*>,q)) = 2

thus len (MergeSequence (<*x,y*>,q)) = len <*x,y*> by Def1

.= 2 by FINSEQ_1:44 ; :: thesis: verum