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 )

hence f . 1 = {}
.= (Rev f) . (len f) by A1 ;
:: thesis: f . (len f) = (Rev f) . 1
thus f . (len f) = {} by A1
.= (Rev f) . 1 by A1 ; :: thesis: verum

end;

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

then len f in Seg (len f) by FINSEQ_1:3;
then len f in dom f by FINSEQ_1:def 3;
hence (Rev f) . (len f) = f . (((len f) - (len f)) + 1) by Th58
.= f . 1 ;
:: thesis: f . (len f) = (Rev f) . 1
len f >= 1 by A3, NAT_1:14;
then 1 in dom f by FINSEQ_3:25;
hence (Rev f) . 1 = f . (((len f) - 1) + 1) by Th58
.= f . (len f) ;
:: thesis: verum

end;

end;