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