let i1, i2 be Nat; for f1 being FinSequence holds mid (f1,i1,i2) = Rev (mid (f1,i2,i1))
let f1 be FinSequence; mid (f1,i1,i2) = Rev (mid (f1,i2,i1))
set k1 = i1;
set k2 = i2;
now ( ( i1 <= i2 & mid (f1,i1,i2) = Rev (mid (f1,i2,i1)) ) or ( i1 > i2 & mid (f1,i1,i2) = Rev (mid (f1,i2,i1)) ) )per cases
( i1 <= i2 or i1 > i2 )
;
case A1:
i1 <= i2
;
mid (f1,i1,i2) = Rev (mid (f1,i2,i1))then A2:
mid (
f1,
i1,
i2)
= (f1 /^ (i1 -' 1)) | ((i2 -' i1) + 1)
by FINSEQ_6:def 3;
now ( ( i1 < i2 & mid (f1,i1,i2) = Rev (mid (f1,i2,i1)) ) or ( i1 = i2 & mid (f1,i1,i2) = Rev (mid (f1,i2,i1)) ) )per cases
( i1 < i2 or i1 = i2 )
by A1, XXREAL_0:1;
case A3:
i1 = i2
;
mid (f1,i1,i2) = Rev (mid (f1,i2,i1))A4:
(
i1 = 0 or
0 + 1
<= i1 )
by NAT_1:13;
now ( ( i1 = 0 & mid (f1,i1,i2) = Rev (mid (f1,i2,i1)) ) or ( 1 <= i1 & i1 <= len f1 & mid (f1,i1,i2) = Rev (mid (f1,i2,i1)) ) or ( len f1 < i1 & mid (f1,i1,i2) = Rev (mid (f1,i2,i1)) ) )end; hence
mid (
f1,
i1,
i2)
= Rev (mid (f1,i2,i1))
;
verum end; end; end; hence
mid (
f1,
i1,
i2)
= Rev (mid (f1,i2,i1))
;
verum end; end; end;
hence
mid (f1,i1,i2) = Rev (mid (f1,i2,i1))
; verum