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 i + k = len f ; :: thesis: Rev (f | k) = (Rev f) /^ i

then A1: i + k = len (Rev f) by FINSEQ_5:def 3;

thus Rev (f | k) = Rev ((Rev (Rev f)) | k)

.= Rev (Rev ((Rev f) /^ i)) by A1, Th84

.= (Rev f) /^ i ; :: thesis: verum

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 i + k = len f ; :: thesis: Rev (f | k) = (Rev f) /^ i

then A1: i + k = len (Rev f) by FINSEQ_5:def 3;

thus Rev (f | k) = Rev ((Rev (Rev f)) | k)

.= Rev (Rev ((Rev f) /^ i)) by A1, Th84

.= (Rev f) /^ i ; :: thesis: verum