let f, g be FinSequence; :: thesis: ( len f >= 1 implies mid ((f ^ g),1,(len f)) = f )
assume A1: len f >= 1 ; :: thesis: mid ((f ^ g),1,(len f)) = f
then (len f) - 1 >= 0 by XREAL_1:48;
then (len f) - 1 = (len f) -' 1 by XREAL_0:def 2;
then A2: ((len f) -' 1) + 1 = len f ;
1 - 1 = 0 ;
then A3: 1 -' 1 = 0 by XREAL_0:def 2;
(f ^ g) | (len f) = f by FINSEQ_5:23;
then ((f ^ g) /^ 0) | (len f) = f by FINSEQ_5:28;
hence mid ((f ^ g),1,(len f)) = f by A1, A2, A3, FINSEQ_6:def 3; :: thesis: verum