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:235;
then A3: ((len f) -' 2) + 1 = (((len f) - 1) - 1) + 1
.= (len f) -' 1 by A1, XREAL_1:235, XXREAL_0:2 ;

now

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:16;
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:122; :: 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:126, XXREAL_0:2;
A7: f | 0 is empty ;
((len f) -' 2) + 1 = ((len f) - 2) + 1 by A1, XREAL_1:235
.= (len f) - 1
.= (len f) -' 1 by A1, XREAL_1:235, XXREAL_0:2 ;
hence f = (f | ((len f) -' 2)) ^ (mid f,((len f) -' 1),(len f)) by A5, A6, A7, FINSEQ_1:47; :: thesis: verum

end;

end;

end;

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