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;
A1: len ((i + 1) |-> a) = i + 1 by FINSEQ_1:def 18;
consider q being FinSequence, x being set such that
A2: (i + 1) |-> a = q ^ <*x*> by FINSEQ_1:63;
A3: len ((i + 1) |-> a) = (len q) + 1 by A2, Th19;
A4: ((i + 1) |-> a) . (i + 1) = a by FINSEQ_1:6, FUNCOP_1:13;

now

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

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

then ( q = {} & len (i |-> a) = 0 ) by A1, A3;
hence q = i |-> a ; :: thesis: verum

end;

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

A6: dom q = Seg (len q) by FINSEQ_1:def 3;
then i in dom q by A1, A3, A5, FINSEQ_1:5;
then ( q . i in rng q & Seg (i + 1) <> {} & (i + 1) |-> a = (Seg (i + 1)) --> a ) by FUNCT_1:def 5;
then ( rng q <> {} & rng q c= rng ((i + 1) |-> a) & rng ((i + 1) |-> a) = {a} ) by A2, FINSEQ_1:42, FUNCOP_1:14;
then rng q = {a} by ZFMISC_1:39;
hence q = i |-> a by A1, A3, A6, FUNCOP_1:15; :: thesis: verum

end;

end;

end;

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