let i be Nat; :: thesis: for a being set holds (i + 1) |-> a = (i |-> a) ^ <*a*>
let a be set ; :: thesis: (i + 1) |-> a = (i |-> a) ^ <*a*>
set p = (i + 1) |-> a;
consider q being FinSequence, x being set such that
A1: (i + 1) |-> a = q ^ <*x*> by FINSEQ_1:63;
A2: ( len ((i + 1) |-> a) = i + 1 & len ((i + 1) |-> a) = (len q) + 1 ) by A1, Th19, FINSEQ_1:def 18;

A3: now

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:42, FUNCOP_1:14;
A7: dom q = Seg (len q) by FINSEQ_1:def 3;
then i in dom q by A2, A5, FINSEQ_1:5;
then q . i in rng q by FUNCT_1:def 5;
then rng q = {a} by A6, ZFMISC_1:39;
hence q = i |-> a by A2, A7, FUNCOP_1:15; :: thesis: verum

end;

end;

end;

((i + 1) |-> a) . (i + 1) = a by FINSEQ_1:6, FUNCOP_1:13;
hence (i + 1) |-> a = (i |-> a) ^ <*a*> by A1, A2, A3, FINSEQ_1:59; :: thesis: verum