let i, j be Nat; :: thesis: for D being non empty set
for f being FinSequence of D st i in dom f & i + j = (len f) + 1 holds
f /. i = (Rev f) /. j
let D be non empty set ; :: thesis: for f being FinSequence of D st i in dom f & i + j = (len f) + 1 holds
f /. i = (Rev f) /. j
let f be FinSequence of D; :: thesis: ( i in dom f & i + j = (len f) + 1 implies f /. i = (Rev f) /. j )
assume that
A1: i in dom f and
A2: i + j = (len f) + 1 ; :: thesis: f /. i = (Rev f) /. j
A3: j in dom (Rev f) by A1, A2, Th59;
A4: i = ((len f) - j) + 1 by A2;
thus f /. i = f . i by A1, PARTFUN1:def 6
.= (Rev f) . j by A4, A3, Def3
.= (Rev f) /. j by A3, PARTFUN1:def 6 ; :: thesis: verum