theorem Th50: :: JORDAN1J:50

for D being set
for f, g being FinSequence of D holds (f ^' g) | (len f) = f