theorem Th36: :: FINSEQ_3:38

for p, q, r being FinSequence st len r = (len p) + (len q) & ( for k being Nat st k in dom p holds
r . k = p . k ) & ( for k being Nat st k in dom q holds
r . ((len p) + k) = q . k ) holds
r = p ^ q