let i, k be Nat; :: thesis: for D being non empty set
for f being FinSequence of D st i + k = len f holds
Rev (f /^ k) = (Rev f) | i

let D be non empty set ; :: thesis: for f being FinSequence of D st i + k = len f holds
Rev (f /^ k) = (Rev f) | i

let f be FinSequence of D; :: thesis: ( i + k = len f implies Rev (f /^ k) = (Rev f) | i )
assume A1: i + k = len f ; :: thesis: Rev (f /^ k) = (Rev f) | i
then A2: k <= len f by NAT_1:11;
i <= len f by ;
then i <= len (Rev f) by FINSEQ_5:def 3;
then A3: len ((Rev f) | i) = (len f) - k by
.= len (f /^ k) by ;
now :: thesis: for j being Nat st j in dom ((Rev f) | i) holds
((Rev f) | i) . j = (f /^ k) . (((len (f /^ k)) - j) + 1)
A4: len (f /^ k) = (len f) - k by ;
let j be Nat; :: thesis: ( j in dom ((Rev f) | i) implies ((Rev f) | i) . j = (f /^ k) . (((len (f /^ k)) - j) + 1) )
A5: dom ((Rev f) | i) c= dom (Rev f) by FINSEQ_5:18;
assume A6: j in dom ((Rev f) | i) ; :: thesis: ((Rev f) | i) . j = (f /^ k) . (((len (f /^ k)) - j) + 1)
then j <= len (f /^ k) by ;
then reconsider m = (len (f /^ k)) - j as Element of NAT by INT_1:5;
j >= 1 by ;
then (len (f /^ k)) - j <= (len (f /^ k)) - 1 by XREAL_1:10;
then A7: ((len (f /^ k)) - j) + 1 <= len (f /^ k) by XREAL_1:19;
1 <= m + 1 by NAT_1:11;
then A8: m + 1 in dom (f /^ k) by ;
thus ((Rev f) | i) . j = ((Rev f) | i) /. j by
.= (Rev f) /. j by
.= (Rev f) . j by
.= f . ((((len (f /^ k)) + k) - j) + 1) by
.= f . ((m + 1) + k)
.= (f /^ k) . (((len (f /^ k)) - j) + 1) by ; :: thesis: verum
end;
hence Rev (f /^ k) = (Rev f) | i by ; :: thesis: verum