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:80 ;
assume A3: i <= len r ; :: thesis: Rev (r /^ i) = (Rev r) | ((len r) -' i)
then (len r) - i >= 0 by XREAL_1:50;
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:27;
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 2 ;
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 A3, RFINSEQ:def 2;
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:50;
then A11: (len r) - k = (len r) -' k by XREAL_0:def 2;
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 A12: ((len r) -' k) + 1 <= len r by A10, XREAL_0:def 2;
((len r) -' k) + 1 > 0 ;
then ((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:27;
A14: r = r /^ 0 by FINSEQ_5:31;
k in dom r by A6, A9, FINSEQ_3:27;
then A15: k in dom (Rev r) by FINSEQ_5:60;
k <= len (r /^ i) by A7, FINSEQ_5:def 3;
then A16: k <= (len r) - i by A3, RFINSEQ:def 2;
then A17: ((len r) -' i) - k >= 0 by A4, XREAL_1:50;
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:121
.= 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: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 >= 0 + 1 & (((len r) -' i) -' k) + 1 <= len (r /^ i) ) by A3, A4, A18, RFINSEQ:def 2, XREAL_1:9;
then (((len r) - i) - k) + 1 in Seg (len (r /^ i)) by A4, A18, FINSEQ_1:3;
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 8
.= (r /^ 0) /. (i + ((((len r) -' i) -' k) + 1)) by A4, A18, A21, A14, FINSEQ_5:30
.= r . (((len r) - k) + 1) by A20, A13, A14, PARTFUN1:def 8 ;
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:42
.= 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:18; :: thesis: verum