:: deftheorem Def3 defines Op-Shift DESCIP_1:def 3 :
for D being non empty set
for s being FinSequence of D
for n being Integer st 1 <= len s holds
for b₄ being FinSequence of D holds
( b₄ = Op-Shift (s,n) iff ( len b₄ = len s & ( for i being Nat st i in Seg (len s) holds
b₄ . i = s . ((((i - 1) + n) mod (len s)) + 1) ) ) );