:: deftheorem Def7 defines ^ FINSEQ_1:def 7 :
for p, q being FinSequence
for b₃ being FinSequence holds
( b₃ = p ^ q iff ( dom b₃ = Seg ((len p) + (len q)) & ( for k being Nat st k in dom p holds
b₃ . k = p . k ) & ( for k being Nat st k in dom q holds
b₃ . ((len p) + k) = q . k ) ) );