theorem Th5: :: DESCIP_1:5

for D being non empty set
for s being FinSequence of D st 1 <= len s holds
( Op-LeftShift s is FinSequence of D & len (Op-LeftShift s) = len s )