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

proof

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 ;
i <= i + 1 by NAT_1:11;
then Seg i c= Seg (i + 1) by FINSEQ_1:7;
then ( j in Seg (i + 1) & (idseq (i + 1)) . j = q . j ) by A1, A2, A3, A5, A6, FINSEQ_1:def 7;
hence q . a = a by FUNCT_1:35; :: thesis: verum

end;

hence idseq (i + 1) = (idseq i) ^ <*(i + 1)*> by A1, A2, A3, A4, A5, FUNCT_1:34; :: thesis: verum