let i be Nat; :: thesis: idseq (i + 1) = (idseq i) ^ <*(i + 1)*>
set p = idseq (i + 1);
consider q being FinSequence, a being set such that
A1: idseq (i + 1) = q ^ <*a*> by FINSEQ_1:63;
A2: ( len (idseq (i + 1)) = i + 1 & len (idseq (i + 1)) = (len q) + 1 ) by A1, Th19, FINSEQ_1:def 18;
A3: dom q = Seg (len q) by FINSEQ_1:def 3;
A4: for a being set st a in Seg i holds
q . a = a

proof

i <= i + 1 by NAT_1:11;
then A5: Seg i c= Seg (i + 1) by FINSEQ_1:7;
let a be set ; :: thesis: ( a in Seg i implies q . a = a )
assume A6: a in Seg i ; :: thesis: q . a = a
then reconsider j = a as Element of NAT ;
(idseq (i + 1)) . j = q . j by A1, A2, A3, A6, FINSEQ_1:def 7;
hence q . a = a by A6, A5, FUNCT_1:35; :: thesis: verum

end;

(idseq (i + 1)) . (i + 1) = i + 1 by FINSEQ_1:6, FUNCT_1:35;
then a = i + 1 by A1, A2, FINSEQ_1:59;
hence idseq (i + 1) = (idseq i) ^ <*(i + 1)*> by A1, A2, A3, A4, FUNCT_1:34; :: thesis: verum