for X being set
for p, q being XFinSequence
for n being Nat st Shift ((p ^ q),n) c= X holds
Shift (p,n) c= X