consider p being FinSequence of bool X such that
len p = card Y and
rng p = Y and
A1: Components Y = { (Intersect (rng (MergeSequence p,q))) where q is FinSequence of BOOLEAN : len q = len p } by Def2;
A2: (len p) -tuples_on BOOLEAN is finite by Th2;
deffunc H₁( Element of BOOLEAN * ) -> Element of bool X = Intersect (rng (MergeSequence p,X));
A3: { H₁(q) where q is Element of BOOLEAN * : q in (len p) -tuples_on BOOLEAN } is finite from FRAENKEL:sch 21(A2);
Components Y c= { (Intersect (rng (MergeSequence p,q))) where q is Element of BOOLEAN * : q in (len p) -tuples_on BOOLEAN }

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in Components Y or z in { (Intersect (rng (MergeSequence p,q))) where q is Element of BOOLEAN * : q in (len p) -tuples_on BOOLEAN } )
assume z in Components Y ; :: thesis: z in { (Intersect (rng (MergeSequence p,q))) where q is Element of BOOLEAN * : q in (len p) -tuples_on BOOLEAN }
then consider q being FinSequence of BOOLEAN such that
A4: z = Intersect (rng (MergeSequence p,q)) and
A5: len q = len p by A1;
A6: q is Element of BOOLEAN * by FINSEQ_1:def 11;
q is Element of (len q) -tuples_on BOOLEAN by FINSEQ_2:110;
hence z in { (Intersect (rng (MergeSequence p,q1))) where q1 is Element of BOOLEAN * : q1 in (len p) -tuples_on BOOLEAN } by A4, A5, A6; :: thesis: verum

end;

hence Components Y is finite by A3; :: thesis: verum