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 ) )
assume A1: not f is empty ; :: thesis: ( f /. 1 = (Rev f) /. (len f) & f /. (len f) = (Rev f) /. 1 )
then A2: 1 in dom f by Th6;
A3: len f in dom f by A1, Th6;
A4: dom f = dom (Rev f) by Th60;
thus f /. 1 = f . 1 by A2, PARTFUN1:def 8
.= (Rev f) . (len f) by Th65
.= (Rev f) /. (len f) by A3, A4, PARTFUN1:def 8 ; :: thesis: f /. (len f) = (Rev f) /. 1
thus f /. (len f) = f . (len f) by A3, PARTFUN1:def 8
.= (Rev f) . 1 by Th65
.= (Rev f) /. 1 by A2, A4, PARTFUN1:def 8 ; :: thesis: verum