theorem :: FINSEQ_5:65

for D being non empty set
for f being FinSequence of D st not f is empty holds
( f /. 1 = (Rev f) /. (len f) & f /. (len f) = (Rev f) /. 1 )