let p, q be FinSequence; :: thesis: for x being object st q <> {} holds
(p ^ <*x*>) $^ q = p ^ q
let x be object ; :: thesis: ( 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 <> {} ; :: thesis: (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; :: thesis: verum