let i be natural Number ; 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
(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; verum