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) )
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 A1: (len (Rev r)) -' i <= len (Rev r) by FINSEQ_5:def 3;
A2: len ((Rev r) | ((len r) -' i)) = len ((Rev r) | ((len (Rev r)) -' i)) by FINSEQ_5:def 3
.= (len (Rev r)) -' i by A1, FINSEQ_1:59 ;
assume A3: i <= len r ; :: thesis: Rev (r /^ i) = (Rev r) | ((len r) -' i)
then (len r) - i >= 0 by XREAL_1:48;
then A4: (len r) - i = (len r) -' i by XREAL_0:def 2;
A5: 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 that
A6: 1 <= k and
A7: k <= len (Rev (r /^ i)) ; :: thesis: (Rev (r /^ i)) . k = ((Rev r) | ((len r) -' i)) . k
k in dom (Rev (r /^ i)) by A6, A7, FINSEQ_3:25;
then A8: (Rev (r /^ i)) . k = (r /^ i) . (((len (r /^ i)) - k) + 1) by FINSEQ_5:def 3
.= (r /^ i) . ((((len r) - i) - k) + 1) by A3, RFINSEQ:def 1 ;
(len r) + 0 <= (len r) + i by XREAL_1:7;
then (len r) - i <= ((len r) + i) - i by XREAL_1:9;
then len (r /^ i) <= len r by A3, RFINSEQ:def 1;
then len (Rev (r /^ i)) <= len r by FINSEQ_5:def 3;
then A9: k <= len r by A7, XXREAL_0:2;
then A10: (len r) - k >= 0 by XREAL_1:48;
then A11: (len r) - k = (len r) -' k by XREAL_0:def 2;
k - 1 >= 0 by A6, XREAL_1:48;
then (len r) + 0 <= (len r) + (k - 1) by XREAL_1:7;
then (len r) - (k - 1) <= ((len r) + (k - 1)) - (k - 1) by XREAL_1:9;
then ((len r) - k) + 1 <= len r ;
then A12: ((len r) -' k) + 1 <= len r by A10, XREAL_0:def 2;
((len r) - k) + 1 >= 0 + 1 by A11, NAT_1:13;
then A13: ((len r) - k) + 1 in dom r by A11, A12, FINSEQ_3:25;
k in dom r by A6, A9, FINSEQ_3:25;
then A15: k in dom (Rev r) by FINSEQ_5:57;
k <= len (r /^ i) by A7, FINSEQ_5:def 3;
then A16: k <= (len r) - i by A3, RFINSEQ:def 1;
then A17: ((len r) -' i) - k >= 0 by A4, XREAL_1:48;
then A18: ((len r) -' i) -' k = ((len r) -' i) - k by XREAL_0:def 2;
k <= (len r) -' i by A16, XREAL_0:def 2;
then A19: ((Rev r) | ((len r) -' i)) . k = (Rev r) . k by FINSEQ_3:112
.= r . (((len r) - k) + 1) by A15, FINSEQ_5:def 3 ;
A20: i + ((((len r) -' i) -' k) + 1) = i + ((((len r) - i) - k) + 1) by A4, A17, XREAL_0:def 2
.= ((((len r) - i) + i) - k) + 1 ;
k - 1 >= 0 by A6, XREAL_1:48;
then ((len r) - i) + 0 <= ((len r) - i) + (k - 1) by XREAL_1:7;
then ((len r) - i) - (k - 1) <= (((len r) - i) + (k - 1)) - (k - 1) by XREAL_1:9;
then ( (((len r) -' i) -' k) + 1 >= 0 + 1 & (((len r) -' i) -' k) + 1 <= len (r /^ i) ) by A3, A4, A18, RFINSEQ:def 1, XREAL_1:7;
then (((len r) - i) - k) + 1 in Seg (len (r /^ i)) by A4, A18, FINSEQ_1:1;
then A21: (((len r) - i) - k) + 1 in dom (r /^ i) by FINSEQ_1:def 3;
then (r /^ i) . ((((len r) - i) - k) + 1) = (r /^ i) /. ((((len r) -' i) -' k) + 1) by A4, A18, PARTFUN1:def 6
.= (r /^ 0) /. (i + ((((len r) -' i) -' k) + 1)) by A4, A18, A21, FINSEQ_5:27
.= r . (((len r) - k) + 1) by A20, A13, PARTFUN1:def 6 ;
hence (Rev (r /^ i)) . k = ((Rev r) | ((len r) -' i)) . k by A8, A19; :: thesis: verum

end;

len (Rev (r /^ i)) = len (r /^ i) by FINSEQ_5:def 3
.= (len r) -' i by RFINSEQ:29
.= len ((Rev r) | ((len r) -' i)) by A2, FINSEQ_5:def 3 ;
hence Rev (r /^ i) = (Rev r) | ((len r) -' i) by A5, FINSEQ_1:14; :: thesis: verum