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