let D be non empty set ; :: thesis: for r being FinSequence of D
for i being Element of NAT st i <= len r holds
Rev (r /^ i) = (Rev r) | ((len r) -' i)
let r be FinSequence of D; :: thesis: for i being Element of NAT st i <= len r holds
Rev (r /^ i) = (Rev r) | ((len r) -' i)
let i be Element of NAT ; :: thesis: ( i <= len r implies Rev (r /^ i) = (Rev r) | ((len r) -' i) )
assume A1: i <= len r ; :: thesis: Rev (r /^ i) = (Rev r) | ((len r) -' i)
then (len r) - i >= 0 by XREAL_1:50;
then A2: (len r) - i = (len r) -' i by XREAL_0:def 2;
set s = Rev r;
(len r) -' i <= len r by NAT_D:50;
then (len r) -' i <= len (Rev r) by FINSEQ_5:def 3;
then A3: (len (Rev r)) -' i <= len (Rev r) by FINSEQ_5:def 3;
A4: len ((Rev r) | ((len r) -' i)) = len ((Rev r) | ((len (Rev r)) -' i)) by FINSEQ_5:def 3
.= (len (Rev r)) -' i by A3, FINSEQ_1:80 ;
A5: len (Rev (r /^ i)) = len (r /^ i) by FINSEQ_5:def 3
.= (len r) -' i by JORDAN3:19
.= len ((Rev r) | ((len r) -' i)) by A4, FINSEQ_5:def 3 ;
for k being Nat st 1 <= k & k <= len (Rev (r /^ i)) holds
(Rev (r /^ i)) . k = ((Rev r) | ((len r) -' i)) . k

proof

let k be Nat; :: thesis: ( 1 <= k & k <= len (Rev (r /^ i)) implies (Rev (r /^ i)) . k = ((Rev r) | ((len r) -' i)) . k )
assume A6: ( 1 <= k & k <= len (Rev (r /^ i)) ) ; :: thesis: (Rev (r /^ i)) . k = ((Rev r) | ((len r) -' i)) . k
then k in dom (Rev (r /^ i)) by FINSEQ_3:27;
then A7: (Rev (r /^ i)) . k = (r /^ i) . (((len (r /^ i)) - k) + 1) by FINSEQ_5:def 3
.= (r /^ i) . ((((len r) - i) - k) + 1) by A1, RFINSEQ:def 2 ;
( 1 <= k & k <= len (r /^ i) ) by A6, FINSEQ_5:def 3;
then A8: ( 1 <= k & k <= (len r) - i ) by A1, RFINSEQ:def 2;
then A9: ((len r) -' i) - k >= 0 by A2, XREAL_1:50;
then A10: ((len r) -' i) -' k = ((len r) -' i) - k by XREAL_0:def 2;
A11: (((len r) -' i) -' k) + 1 >= 0 + 1 by XREAL_1:9;
k - 1 >= 0 by A6, XREAL_1:50;
then ((len r) - i) + 0 <= ((len r) - i) + (k - 1) by XREAL_1:9;
then ((len r) - i) - (k - 1) <= (((len r) - i) + (k - 1)) - (k - 1) by XREAL_1:11;
then (((len r) -' i) -' k) + 1 <= len (r /^ i) by A1, A2, A10, RFINSEQ:def 2;
then (((len r) - i) - k) + 1 in Seg (len (r /^ i)) by A2, A10, A11, FINSEQ_1:3;
then A12: (((len r) - i) - k) + 1 in dom (r /^ i) by FINSEQ_1:def 3;
A13: i + ((((len r) -' i) -' k) + 1) = i + ((((len r) - i) - k) + 1) by A2, A9, XREAL_0:def 2
.= ((((len r) - i) + i) - k) + 1 ;
0 <= i by NAT_1:2;
then (len r) + 0 <= (len r) + i by XREAL_1:9;
then (len r) - i <= ((len r) + i) - i by XREAL_1:11;
then len (r /^ i) <= len r by A1, RFINSEQ:def 2;
then len (Rev (r /^ i)) <= len r by FINSEQ_5:def 3;
then A14: k <= len r by A6, XXREAL_0:2;
then A15: (len r) - k >= 0 by XREAL_1:50;
then A16: (len r) - k = (len r) -' k by XREAL_0:def 2;
((len r) -' k) + 1 > 0 ;
then A17: ((len r) - k) + 1 >= 0 + 1 by A16, NAT_1:13;
k - 1 >= 0 by A6, XREAL_1:50;
then (len r) + 0 <= (len r) + (k - 1) by XREAL_1:9;
then (len r) - (k - 1) <= ((len r) + (k - 1)) - (k - 1) by XREAL_1:11;
then ((len r) - k) + 1 <= len r ;
then ((len r) -' k) + 1 <= len r by A15, XREAL_0:def 2;
then A18: ((len r) - k) + 1 in dom r by A16, A17, FINSEQ_3:27;
A19: r = r /^ 0 by FINSEQ_5:31;
A20: (r /^ i) . ((((len r) - i) - k) + 1) = (r /^ i) /. ((((len r) -' i) -' k) + 1) by A2, A10, A12, PARTFUN1:def 8
.= (r /^ 0 ) /. (i + ((((len r) -' i) -' k) + 1)) by A2, A10, A12, A19, FINSEQ_5:30
.= r . (((len r) - k) + 1) by A13, A18, A19, PARTFUN1:def 8 ;
k in dom r by A6, A14, FINSEQ_3:27;
then A21: k in dom (Rev r) by FINSEQ_5:60;
k <= (len r) -' i by A8, XREAL_0:def 2;
then ((Rev r) | ((len r) -' i)) . k = (Rev r) . k by FINSEQ_3:121
.= r . (((len r) - k) + 1) by A21, FINSEQ_5:def 3 ;
hence (Rev (r /^ i)) . k = ((Rev r) | ((len r) -' i)) . k by A7, A20; :: thesis: verum

end;

hence Rev (r /^ i) = (Rev r) | ((len r) -' i) by A5, FINSEQ_1:18; :: thesis: verum