let f1, f2 be FinSequence of bool F; :: thesis: ( dom f1 = dom A & ( for k being Element of NAT st k in dom f1 holds
( ( i = k implies f1 . k = (A . k) \ {x} ) & ( i <> k implies f1 . k = A . k ) ) ) & dom f2 = dom A & ( for k being Element of NAT st k in dom f2 holds
( ( i = k implies f2 . k = (A . k) \ {x} ) & ( i <> k implies f2 . k = A . k ) ) ) implies f1 = f2 )
assume that
A1: dom f1 = dom A and
A2: for k being Element of NAT st k in dom f1 holds
( ( i = k implies f1 . k = (A . k) \ {x} ) & ( i <> k implies f1 . k = A . k ) ) and
A3: dom f2 = dom A and
A4: for k being Element of NAT st k in dom f2 holds
( ( i = k implies f2 . k = (A . k) \ {x} ) & ( i <> k implies f2 . k = A . k ) ) ; :: thesis: f1 = f2
for z being Nat st z in dom f1 holds
f1 . z = f2 . z

proof

let z be Nat; :: thesis: ( z in dom f1 implies f1 . z = f2 . z )
assume A5: z in dom f1 ; :: thesis: f1 . z = f2 . z

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

suppose A6: z = i ; :: thesis: f1 . z = f2 . z

then f1 . z = (A . i) \ {x} by A2, A5
.= f2 . z by A1, A3, A4, A5, A6 ;
hence f1 . z = f2 . z ; :: thesis: verum

end;

suppose A7: z <> i ; :: thesis: f1 . z = f2 . z

then f1 . z = A . z by A2, A5
.= f2 . z by A1, A3, A4, A5, A7 ;
hence f1 . z = f2 . z ; :: thesis: verum

end;

end;

end;

hence f1 = f2 by A1, A3, FINSEQ_1:13; :: thesis: verum