let D be non empty set ; :: thesis: for f being FinSequence of D st 2 <= len f holds
f = (f | ((len f) -' 2)) ^ (mid (f,((len f) -' 1),(len f)))
let f be FinSequence of D; :: thesis: ( 2 <= len f implies f = (f | ((len f) -' 2)) ^ (mid (f,((len f) -' 1),(len f))) )
assume A1: 2 <= len f ; :: thesis: f = (f | ((len f) -' 2)) ^ (mid (f,((len f) -' 1),(len f)))
then A2: (len f) -' 2 = (len f) - 2 by XREAL_1:233;
then A3: ((len f) -' 2) + 1 = (((len f) - 1) - 1) + 1
.= (len f) -' 1 by A1, XREAL_1:233, XXREAL_0:2 ;

now :: thesis: ( ( (len f) -' 2 > 0 & f = (f | ((len f) -' 2)) ^ (mid (f,((len f) -' 1),(len f))) ) or ( (len f) -' 2 = 0 & f = (f | ((len f) -' 2)) ^ (mid (f,((len f) -' 1),(len f))) ) )

per cases ( (len f) -' 2 > 0 or (len f) -' 2 = 0 ) ;

case (len f) -' 2 > 0 ; :: thesis: f = (f | ((len f) -' 2)) ^ (mid (f,((len f) -' 1),(len f)))

then A4: 0 + 1 <= (len f) -' 2 by NAT_1:13;
len f < (len f) + 1 by NAT_1:13;
then len f < ((len f) + 1) + 1 by NAT_1:13;
then (len f) - 2 < ((len f) + 2) - 2 by XREAL_1:14;
then f = (mid (f,1,((len f) -' 2))) ^ (mid (f,(((len f) -' 2) + 1),(len f))) by A2, A4, Th5;
hence f = (f | ((len f) -' 2)) ^ (mid (f,((len f) -' 1),(len f))) by A3, A4, FINSEQ_6:116; :: thesis: verum

end;

case A5: (len f) -' 2 = 0 ; :: thesis: f = (f | ((len f) -' 2)) ^ (mid (f,((len f) -' 1),(len f)))

then A6: mid (f,(((len f) -' 2) + 1),(len f)) = f by A1, FINSEQ_6:120, XXREAL_0:2;
A7: f | 0 is empty ;
((len f) -' 2) + 1 = ((len f) - 2) + 1 by A1, XREAL_1:233
.= (len f) - 1
.= (len f) -' 1 by A1, XREAL_1:233, XXREAL_0:2 ;
hence f = (f | ((len f) -' 2)) ^ (mid (f,((len f) -' 1),(len f))) by A5, A6, A7, FINSEQ_1:34; :: thesis: verum

end;

end;

end;

hence f = (f | ((len f) -' 2)) ^ (mid (f,((len f) -' 1),(len f))) ; :: thesis: verum