theorem Th18: :: DESCIP_1:18

for D being non empty set
for s being FinSequence of D
for n, m being Nat st n + m <= len s holds
(s | n) ^ ((s /^ n) | m) = s | (n + m)