let D be non empty set ; :: thesis: for f being FinSequence of D st not f is empty holds
( f /. 1 = (Rev f) /. (len f) & f /. (len f) = (Rev f) /. 1 )
let f be FinSequence of D; :: thesis: ( not f is empty implies ( f /. 1 = (Rev f) /. (len f) & f /. (len f) = (Rev f) /. 1 ) )
A1: dom f = dom (Rev f) by Th57;
assume A2: not f is empty ; :: thesis: ( f /. 1 = (Rev f) /. (len f) & f /. (len f) = (Rev f) /. 1 )
then A3: len f in dom f by Th6;
1 in dom f by A2, Th6;
hence f /. 1 = f . 1 by PARTFUN1:def 6
.= (Rev f) . (len f) by Th62
.= (Rev f) /. (len f) by A3, A1, PARTFUN1:def 6 ;
:: thesis: f /. (len f) = (Rev f) /. 1
thus f /. (len f) = f . (len f) by A3, PARTFUN1:def 6
.= (Rev f) . 1 by Th62
.= (Rev f) /. 1 by A2, A1, Th6, PARTFUN1:def 6 ; :: thesis: verum