:: deftheorem defines Shift MODELC_2:def 42 :
for S being non empty set
for t being set
for k being Nat holds Shift (t,k,S) = CastSeq ((CastSeq (t,S)) ^\ k);