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 )
assume q <> {} ; :: thesis: (p ^ <*x*>) $^ q = p ^ q
then consider i being Element of NAT , r being FinSequence such that
A1: ( len (p ^ <*x*>) = i + 1 & r = (p ^ <*x*>) | (Seg i) & (p ^ <*x*>) $^ q = r ^ q ) by Def1;
consider s being FinSequence such that
A2: p ^ <*x*> = r ^ s by A1, TREES_1:3;
len <*x*> = 1 by FINSEQ_1:57;
then A3: len (p ^ <*x*>) = (len p) + 1 by FINSEQ_1:35;
then ( len p = i & i <= i + 1 ) by A1, NAT_1:11;
then A4: len r = i by A1, FINSEQ_1:21;
then consider t being FinSequence such that
A5: p ^ t = r by A1, A2, A3, FINSEQ_1:64;
(len r) + 0 = (len p) + (len t) by A5, FINSEQ_1:35;
then t = {} by A1, A3, A4;
hence (p ^ <*x*>) $^ q = p ^ q by A1, A5, FINSEQ_1:47; :: thesis: verum