theorem Th4: :: DESCIP_1:4

for s being FinSequence st 1 <= len s holds
len (Op-LeftShift s) = len s