:: deftheorem Def5 defines Shift LOPBAN_4:def 5 :
for X being non empty ZeroStr
for seq, b₃ being sequence of X holds
( b₃ = Shift seq iff ( b₃ . 0 = 0. X & ( for k being Nat holds b₃ . (k + 1) = seq . k ) ) );