:: deftheorem Def1 defines $^ REWRITE1:def 1 :
for p, q, b₃ being FinSequence holds
( ( ( p = {} or q = {} ) implies ( b₃ = p $^ q iff b₃ = p ^ q ) ) & ( p = {} or q = {} or ( b₃ = p $^ q iff ex i being Nat ex r being FinSequence st
( len p = i + 1 & r = p | (Seg i) & b₃ = r ^ q ) ) ) );