theorem Th51: :: VALUED_1:52

for i being Nat
for p, q being FinSubsequence st q c= p holds
Shift (q,i) c= Shift (p,i)