let f be XFinSequence; :: thesis: mid (f,2,(len f)) = f /^ 1
A1: 2 - 1 >= 0 ;
thus mid (f,2,(len f)) = f /^ 1 by A1, XREAL_0:def 2; :: thesis: verum