consider p being FinSequence such that

A1: rng p = Y and

A2: p is one-to-one by FINSEQ_4:58;

reconsider p = p as FinSequence of bool X by A1, FINSEQ_1:def 4;

reconsider C = { (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p } as Subset-Family of X by Th12;

take C ; :: thesis: ex p being FinSequence of bool X st

( len p = card Y & rng p = Y & C = { (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p } )

take p ; :: thesis: ( len p = card Y & rng p = Y & C = { (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p } )

thus ( len p = card Y & rng p = Y & C = { (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p } ) by A1, A2, FINSEQ_4:62; :: thesis: verum

A1: rng p = Y and

A2: p is one-to-one by FINSEQ_4:58;

reconsider p = p as FinSequence of bool X by A1, FINSEQ_1:def 4;

reconsider C = { (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p } as Subset-Family of X by Th12;

take C ; :: thesis: ex p being FinSequence of bool X st

( len p = card Y & rng p = Y & C = { (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p } )

take p ; :: thesis: ( len p = card Y & rng p = Y & C = { (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p } )

thus ( len p = card Y & rng p = Y & C = { (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p } ) by A1, A2, FINSEQ_4:62; :: thesis: verum