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

now

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

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

then A3: 0 + 1 <= (len f) -' 1 by NAT_1:13;
len f < (len f) + 1 by NAT_1:13;
then (len f) - 1 < ((len f) + 1) - 1 by XREAL_1:16;
then f = (mid f,1,((len f) -' 1)) ^ (mid f,(((len f) -' 1) + 1),(len f)) by A2, A3, Th5;
hence f = (f | ((len f) -' 1)) ^ (mid f,(len f),(len f)) by A2, A3, JORDAN3:25; :: thesis: verum

end;

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

A5: f | 0 is empty ;
mid f,(((len f) -' 1) + 1),(len f) = f by A1, A4, JORDAN3:29;
hence f = (f | ((len f) -' 1)) ^ (mid f,(len f),(len f)) by A2, A4, A5, FINSEQ_1:47; :: thesis: verum

end;

end;

end;

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