theorem :: MODELC_2:79

for S being non empty set
for t being Element of Inf_seq S holds Shift (t,0) = t by Lm28;