let f be FinSequence of NAT ; :: thesis: for j, b being Nat st b <> j holds
(f ^ <*b*>) " {j} = f " {j}
let j, b be Nat; :: thesis: ( b <> j implies (f ^ <*b*>) " {j} = f " {j} )
assume A130: b <> j ; :: thesis: (f ^ <*b*>) " {j} = f " {j}
for z being object holds
( z in (f ^ <*b*>) " {j} iff z in f " {j} )

proof

let z be object ; :: thesis: ( z in (f ^ <*b*>) " {j} iff z in f " {j} )

hereby :: thesis: ( z in f " {j} implies z in (f ^ <*b*>) " {j} )

assume A200: z in (f ^ <*b*>) " {j} ; :: thesis: z in f " {j}
then A210: ( z in dom (f ^ <*b*>) & (f ^ <*b*>) . z in {j} ) by FUNCT_1:def 7;
A240: ( not z in dom (f ^ <*b*>) or z in dom f or ex n being Nat st
( n in dom <*b*> & z = (len f) + n ) ) by FINSEQ_1:25;
A260: for n being Nat holds
( not n in dom <*b*> or not z = (len f) + n )

proof

now :: thesis: for n1 being Nat holds
( not n1 in dom <*b*> or not z = (len f) + n1 )

given n1 being Nat such that B10: ( n1 in dom <*b*> & z = (len f) + n1 ) ; :: thesis: contradiction
dom <*b*> = Seg 1 by FINSEQ_1:def 8;
then n1 = 1 by B10, FINSEQ_1:2, TARSKI:def 1;
then B50: (f ^ <*b*>) . z = b by B10, FINSEQ_1:42;
not b in {j} by A130, TARSKI:def 1;
hence contradiction by B50, FUNCT_1:def 7, A200; :: thesis: verum

end;

hence for n being Nat holds
( not n in dom <*b*> or not z = (len f) + n ) ; :: thesis: verum

end;

(f ^ <*b*>) . z = f . z by A240, FUNCT_1:def 7, A200, A260, FINSEQ_1:def 7;
hence z in f " {j} by A240, A210, A260, FUNCT_1:def 7; :: thesis: verum

end;

assume z in f " {j} ; :: thesis: z in (f ^ <*b*>) " {j}
then A310: ( z in dom f & f . z in {j} ) by FUNCT_1:def 7;
A315: dom f c= dom (f ^ <*b*>) by FINSEQ_1:26;
f . z = (f ^ <*b*>) . z by A310, FINSEQ_1:def 7;
hence z in (f ^ <*b*>) " {j} by A315, A310, FUNCT_1:def 7; :: thesis: verum

end;

hence (f ^ <*b*>) " {j} = f " {j} by TARSKI:2; :: thesis: verum