let i be natural Number ; :: thesis: idseq (i + 1) = (idseq i) ^ <*(i + 1)*>
set p = idseq (i + 1);
consider q being FinSequence, a being object such that
A1: idseq (i + 1) = q ^ <*a*> by FINSEQ_1:46;
A2: ( len (idseq (i + 1)) = i + 1 & len (idseq (i + 1)) = (len q) + 1 ) by A1, Th14, CARD_1:def 7;
A3: dom q = Seg (len q) by FINSEQ_1:def 3;
A4: for a being object 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:5;
let a be object ; :: thesis: ( a in Seg i implies q . a = a )
assume A6: a in Seg i ; :: thesis: q . a = a
then ex j being Nat st
( a = j & 1 <= j & j <= i ) ;
then reconsider j = a as 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:18; :: thesis: verum

end;

(idseq (i + 1)) . (i + 1) = i + 1 by FINSEQ_1:4, FUNCT_1:18;
then a = i + 1 by A1, A2, FINSEQ_1:42;
hence idseq (i + 1) = (idseq i) ^ <*(i + 1)*> by A1, A2, A3, A4, FUNCT_1:17; :: thesis: verum