A . i c= F

proof

per cases ( i in dom A or not i in dom A ) ;

suppose i in dom A ; :: thesis: A . i c= F

then A . i in bool F by FINSEQ_2:11;
hence A . i c= F ; :: thesis: verum

end;

suppose not i in dom A ; :: thesis: A . i c= F

then A . i = {} by FUNCT_1:def 2;
hence A . i c= F ; :: thesis: verum

end;

end;

end;

then reconsider EX = (A . i) \ {x} as Subset of F by XBOOLE_1:1;
set XX = A +* (i,EX);
reconsider XX = A +* (i,EX) as FinSequence of bool F ;
take XX ; :: thesis: ( dom XX = dom A & ( for k being Element of NAT st k in dom XX holds
( ( i = k implies XX . k = (A . k) \ {x} ) & ( i <> k implies XX . k = A . k ) ) ) )
dom XX = dom A by FUNCT_7:30;
hence ( dom XX = dom A & ( for k being Element of NAT st k in dom XX holds
( ( i = k implies XX . k = (A . k) \ {x} ) & ( i <> k implies XX . k = A . k ) ) ) ) by FUNCT_7:31, FUNCT_7:32; :: thesis: verum