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 2, RELAT_1:38
.= (Rev f) . (len f) by A2, FUNCT_1:def 2 ; :: thesis: f . (len f) = (Rev f) . 1
thus f . (len f) = {} by A1, FUNCT_1:def 2, RELAT_1:38
.= (Rev f) . 1 by A2, FUNCT_1:def 2 ; :: 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 Th61
.= 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 Th61
.= f . (len f) ;
:: thesis: verum

end;

end;