let D be non empty set ; 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; ( 1 <= len f implies f = (f | ((len f) -' 1)) ^ (mid (f,(len f),(len f))) )
assume A1:
1 <= len f
; f = (f | ((len f) -' 1)) ^ (mid (f,(len f),(len f)))
then A2:
(len f) -' 1 = (len f) - 1
by XREAL_1:233;
now ( ( (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
;
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;
verum end; end; end;
hence
f = (f | ((len f) -' 1)) ^ (mid (f,(len f),(len f)))
; verum