let f be FinSequence; :: thesis: ( 2 <= len f implies (f /^ 1) . (len (f /^ 1)) = f . (len f) )
assume A1: 2 <= len f ; :: thesis: (f /^ 1) . (len (f /^ 1)) = f . (len f)
set g = f /^ 1;
A2: 1 <= len f by A1, XXREAL_0:2;
then A3: (len (f /^ 1)) + 1 = ((len f) - 1) + 1 by RFINSEQ:def 1
.= len f ;
then 2 - 1 <= ((len (f /^ 1)) + 1) - 1 by A1, XREAL_1:13;
then len (f /^ 1) in Seg (len (f /^ 1)) by FINSEQ_1:3;
then len (f /^ 1) in dom (f /^ 1) by FINSEQ_1:def 3;
hence (f /^ 1) . (len (f /^ 1)) = f . (len f) by A3, A2, RFINSEQ:def 1; :: thesis: verum