consider x being Element of A . i;
( A . i in bool F & x in A . i ) by A1, A2, PARTFUN1:27;
then reconsider E = {x} as Subset of F by ZFMISC_1:37;
reconsider G = A +* i,E as FinSequence of bool F ;
A3: for j being Element of NAT st j in dom A holds
G . j c= A . j

proof

let j be Element of NAT ; :: thesis: ( j in dom A implies G . j c= A . j )
assume j in dom A ; :: thesis: G . j c= A . j

per cases ( j = i or j <> i ) ;

suppose A4: j = i ; :: thesis: G . j c= A . j

G . i = {x} by A1, FUNCT_7:33;
hence G . j c= A . j by A2, A4, ZFMISC_1:37; :: thesis: verum

end;

suppose j <> i ; :: thesis: G . j c= A . j

hence G . j c= A . j by FUNCT_7:34; :: thesis: verum

end;

end;

end;

G . i = {x} by A1, FUNCT_7:33;
then A5: card (G . i) = 1 by CARD_2:60;
dom G = dom A by FUNCT_7:32;
then G is Reduction of A by A3, Def6;
hence ex b₁ being Reduction of A st card (b₁ . i) = 1 by A5; :: thesis: verum