:: deftheorem defines Shift MODELC_2:def 43 :
for S being non empty set
for t being Element of Inf_seq S
for k being Nat holds Shift (t,k) = Shift (t,k,S);