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;

deffunc H_{1}( Element of BOOLEAN * ) -> Element of bool X = Intersect (rng (MergeSequence (p,X)));

A2: Components Y c= { (Intersect (rng (MergeSequence (p,q)))) where q is Element of BOOLEAN * : q in (len p) -tuples_on BOOLEAN }

{ H_{1}(q) where q is Element of BOOLEAN * : q in (len p) -tuples_on BOOLEAN } is finite
from FRAENKEL:sch 21(A4);

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

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;

deffunc H

A2: Components Y c= { (Intersect (rng (MergeSequence (p,q)))) where q is Element of BOOLEAN * : q in (len p) -tuples_on BOOLEAN }

proof

A4:
(len p) -tuples_on BOOLEAN is finite
;
let z be object ; :: 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

A3: ( z = Intersect (rng (MergeSequence (p,q))) & len q = len p ) by A1;

( q is Element of BOOLEAN * & q is Element of (len q) -tuples_on BOOLEAN ) by FINSEQ_1:def 11, FINSEQ_2:92;

hence z in { (Intersect (rng (MergeSequence (p,q)))) where q is Element of BOOLEAN * : q in (len p) -tuples_on BOOLEAN } by A3; :: thesis: verum

end;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

A3: ( z = Intersect (rng (MergeSequence (p,q))) & len q = len p ) by A1;

( q is Element of BOOLEAN * & q is Element of (len q) -tuples_on BOOLEAN ) by FINSEQ_1:def 11, FINSEQ_2:92;

hence z in { (Intersect (rng (MergeSequence (p,q)))) where q is Element of BOOLEAN * : q in (len p) -tuples_on BOOLEAN } by A3; :: thesis: verum

{ H

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