let i be natural Number ; :: thesis:
let a be object ; :: thesis:
set p = (i + 1) |-> a;
consider q being FinSequence, x being object such that
A1: (i + 1) |-> a = q ^ <*x*> by FINSEQ_1:46;
A2: ( len ((i + 1) |-> a) = i + 1 & len ((i + 1) |-> a) = (len q) + 1 ) by A1, Th14, CARD_1:def 7;

A3: now :: thesis:

suppose A4: i = 0 ; :: thesis:

then q = {} by A2;
hence q = i |-> a by A4; :: thesis:

end;

suppose A5: i <> 0 ; :: thesis:

A6: ( rng q c= rng ((i + 1) |-> a) & rng ((i + 1) |-> a) = {a} ) by A1, FINSEQ_1:29, FUNCOP_1:8;
A7: dom q = Seg (len q) by FINSEQ_1:def 3;
then i in dom q by A2, A5, FINSEQ_1:3;
then q . i in rng q by FUNCT_1:def 3;
then rng q = {a} by A6, ZFMISC_1:33;
hence q = i |-> a by A2, A7, FUNCOP_1:9; :: thesis:

end;

end;

end;

((i + 1) |-> a) . (i + 1) = a by FINSEQ_1:4, FUNCOP_1:7;
hence (i + 1) |-> a = (i |-> a) ^ <*a*> by A1, A2, A3, FINSEQ_1:42; :: thesis: