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:233;

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

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:14;
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, FINSEQ_6:116; :: 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, FINSEQ_6:120;
hence f = (f | ((len f) -' 1)) ^ (mid (f,(len f),(len f))) by A2, A4, A5, FINSEQ_1:34; :: thesis: verum

end;

end;

end;

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