set x = the Element of A . i;
( A . i in bool F & the Element of A . i in A . i ) by A1, A2, PARTFUN1:4;
then reconsider E = { the Element of A . i} as Subset of F by ZFMISC_1:31;
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 = { the Element of A . i} by A1, FUNCT_7:31;
hence G . j c= A . j by A2, A4, ZFMISC_1:31; :: thesis: verum

end;

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

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

end;

end;

end;

G . i = { the Element of A . i} by A1, FUNCT_7:31;
then A5: card (G . i) = 1 by CARD_2:42;
dom G = dom A by FUNCT_7:30;
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