theorem Th7: :: DESCIP_1:7

for s being FinSequence holds len (Op-RightShift s) = len s