let f be FinSequence; :: thesis: ( f . 1 = (Rev f) . (len f) & f . (len f) = (Rev f) . 1 )

per cases ( f is empty or not f is empty ) ;

suppose A1: f is empty ; :: thesis: ( f . 1 = (Rev f) . (len f) & f . (len f) = (Rev f) . 1 )

then A2: dom (Rev f) = {} ;
thus f . 1 = {} by A1, FUNCT_1:def 4, RELAT_1:60
.= (Rev f) . (len f) by A2, FUNCT_1:def 4 ; :: thesis: f . (len f) = (Rev f) . 1
thus f . (len f) = {} by A1, FUNCT_1:def 4, RELAT_1:60
.= (Rev f) . 1 by A2, FUNCT_1:def 4 ; :: thesis: verum

end;

suppose not f is empty ; :: thesis: ( f . 1 = (Rev f) . (len f) & f . (len f) = (Rev f) . 1 )

then A3: len f <> 0 ;
then len f in Seg (len f) by FINSEQ_1:5;
then len f in dom f by FINSEQ_1:def 3;
hence (Rev f) . (len f) = f . (((len f) - (len f)) + 1) by Th61
.= f . 1 ;
:: thesis: f . (len f) = (Rev f) . 1
( 1 >= 1 & len f >= 1 ) by A3, NAT_1:14;
then 1 in dom f by FINSEQ_3:27;
hence (Rev f) . 1 = f . (((len f) - 1) + 1) by Th61
.= f . (len f) ;
:: thesis: verum

end;

end;