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

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

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

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

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

.= 3 by FINSEQ_1:45 ; :: thesis: verum

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

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

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

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

.= 3 by FINSEQ_1:45 ; :: thesis: verum