deffunc H₁( object ) -> set = { the Element of A . $1};
A2: for x being object st x in dom A holds
H₁(x) in bool F

proof

let x be object ; :: thesis: ( x in dom A implies H₁(x) in bool F )
assume A3: x in dom A ; :: thesis: H₁(x) in bool F
then A . x <> {} by A1, Th2;
then A4: { the Element of A . x} c= A . x by ZFMISC_1:31;
A . x in bool F by A3, PARTFUN1:4;
then { the Element of A . x} c= F by A4, XBOOLE_1:1;
hence H₁(x) in bool F ; :: thesis: verum

end;

ex f being Function of (dom A),(bool F) st
for x being object st x in dom A holds
f . x = H₁(x) from FUNCT_2:sch 2(A2);
then consider f being Function of (dom A),(bool F) such that
A5: for x being object st x in dom A holds
f . x = H₁(x) ;
A6: for i being Element of NAT st i in dom f holds
f . i = { the Element of A . i}

proof

let i be Element of NAT ; :: thesis: ( i in dom f implies f . i = { the Element of A . i} )
assume i in dom f ; :: thesis: f . i = { the Element of A . i}
then i in dom A by FUNCT_2:def 1;
hence f . i = { the Element of A . i} by A5; :: thesis: verum

end;

A7: dom f = dom A by FUNCT_2:def 1;
A8: for i being Element of NAT st i in dom A holds
f . i c= A . i

proof

let i be Element of NAT ; :: thesis: ( i in dom A implies f . i c= A . i )
assume A9: i in dom A ; :: thesis: f . i c= A . i
then A . i <> {} by A1, Th2;
then { the Element of A . i} c= A . i by ZFMISC_1:31;
hence f . i c= A . i by A7, A6, A9; :: thesis: verum

end;

dom f = dom A by FUNCT_2:def 1
.= Seg (len A) by FINSEQ_1:def 3 ;
then A10: f is FinSequence by FINSEQ_1:def 2;
rng f c= bool F by RELAT_1:def 19;
then f is FinSequence of bool F by A10, FINSEQ_1:def 4;
then reconsider f = f as Reduction of A by A7, A8, Def6;
for i being Element of NAT st i in dom A holds
card (f . i) = 1

proof

let i be Element of NAT ; :: thesis: ( i in dom A implies card (f . i) = 1 )
assume i in dom A ; :: thesis: card (f . i) = 1
then i in dom f by FUNCT_2:def 1;
then f . i = { the Element of A . i} by A6;
hence card (f . i) = 1 by CARD_2:42; :: thesis: verum

end;

hence ex b₁ being Reduction of A st
for i being Element of NAT st i in dom A holds
card (b₁ . i) = 1 ; :: thesis: verum