let i be natural Number ; :: thesis: for a being object holds (i + 1) |-> a = (i |-> a) ^ <*a*>
let a be object ; :: thesis: (i + 1) |-> a = (i |-> a) ^ <*a*>
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: q = i |-> a

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

suppose A4: i = 0 ; :: thesis: q = i |-> a

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

end;

suppose A5: i <> 0 ; :: thesis: q = i |-> a

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: verum

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: verum