theorem Th62: :: FINSEQ_5:62

for f being FinSequence holds
( f . 1 = (Rev f) . (len f) & f . (len f) = (Rev f) . 1 )