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} )

(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

hence
(f ^ <*b*>) " {j} = f " {j}
by TARSKI:2; :: thesis: verum
let z be object ; :: thesis: ( z in (f ^ <*b*>) " {j} iff z in f " {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;hereby :: thesis: ( z in f " {j} implies z in (f ^ <*b*>) " {j} )

assume
z in f " {j}
; :: thesis: 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 )

hence z in f " {j} by A240, A210, A260, FUNCT_1:def 7; :: thesis: verum

end;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

( 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;now :: thesis: for n1 being Nat holds

( not n1 in dom <*b*> or not z = (len f) + n1 )

hence
for n 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;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

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

hence z in f " {j} by A240, A210, A260, FUNCT_1:def 7; :: thesis: verum

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