theorem Th18: :: FILEREC1:18

for D being non empty set
for r being FinSequence of D
for i being Element of NAT st i <= len r holds
Rev (r /^ i) = (Rev r) | ((len r) -' i)