let q, p be FinSequence; :: thesis: for x being set st q <> {} holds
(p ^ <*x*>) $^ q = p ^ q
let x be set ; :: thesis: ( q <> {} implies (p ^ <*x*>) $^ q = p ^ q )
len <*x*> = 1 by FINSEQ_1:57;
then A1: len (p ^ <*x*>) = (len p) + 1 by FINSEQ_1:35;
assume q <> {} ; :: thesis: (p ^ <*x*>) $^ q = p ^ q
then consider i being Element of 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:21;
ex s being FinSequence st p ^ <*x*> = r ^ s by A3, FINSEQ_1:101;
then consider t being FinSequence such that
A6: p ^ t = r by A2, A1, A5, FINSEQ_1:64;
(len r) + 0 = (len p) + (len t) by A6, FINSEQ_1:35;
then t = {} by A2, A1, A5;
hence (p ^ <*x*>) $^ q = p ^ q by A4, A6, FINSEQ_1:47; :: thesis: verum