theorem LemP: :: MSAFREE5:4

for i being Nat
for p, q being FinSequence st i <= len p holds
(p ^ q) | (Seg i) = p | (Seg i)