let p, q be FinSequence; for x being object st q <> {} holds
(p ^ <*x*>) $^ q = p ^ q
let x be object ; ( q <> {} implies (p ^ <*x*>) $^ q = p ^ q )
len <*x*> = 1
by FINSEQ_1:40;
then A1:
len (p ^ <*x*>) = (len p) + 1
by FINSEQ_1:22;
assume
q <> {}
; (p ^ <*x*>) $^ q = p ^ q
then consider i being Nat, r being FinSequence such that
A2:
len (p ^ <*x*>) = i + 1
and
A3:
r = (p ^ <*x*>) | (Seg i)
and
A4:
(p ^ <*x*>) $^ q = r ^ q
by Def1;
i <= i + 1
by NAT_1:11;
then A5:
len r = i
by A2, A3, FINSEQ_1:17;
ex s being FinSequence st p ^ <*x*> = r ^ s
by A3, FINSEQ_1:80;
then consider t being FinSequence such that
A6:
p ^ t = r
by A2, A1, A5, FINSEQ_1:47;
(len r) + 0 = (len p) + (len t)
by A6, FINSEQ_1:22;
then
t = {}
by A2, A1, A5;
hence
(p ^ <*x*>) $^ q = p ^ q
by A4, A6, FINSEQ_1:34; verum