let D be non empty set ; :: thesis: for f being FinSequence of D
for i being Nat st 1 <= i & i < len f holds
Swap f,i,(len f) = (((f | (i -' 1)) ^ <*(f /. (len f))*>) ^ ((f /^ i) | (((len f) -' i) -' 1))) ^ <*(f /. i)*>
let f be FinSequence of D; :: thesis: for i being Nat st 1 <= i & i < len f holds
Swap f,i,(len f) = (((f | (i -' 1)) ^ <*(f /. (len f))*>) ^ ((f /^ i) | (((len f) -' i) -' 1))) ^ <*(f /. i)*>
let i be Nat; :: thesis: ( 1 <= i & i < len f implies Swap f,i,(len f) = (((f | (i -' 1)) ^ <*(f /. (len f))*>) ^ ((f /^ i) | (((len f) -' i) -' 1))) ^ <*(f /. i)*> )
assume ( 1 <= i & i < len f ) ; :: thesis: Swap f,i,(len f) = (((f | (i -' 1)) ^ <*(f /. (len f))*>) ^ ((f /^ i) | (((len f) -' i) -' 1))) ^ <*(f /. i)*>
then Swap f,i,(len f) = ((((f | (i -' 1)) ^ <*(f /. (len f))*>) ^ ((f /^ i) | (((len f) -' i) -' 1))) ^ <*(f /. i)*>) ^ (f /^ (len f)) by Th29
.= ((((f | (i -' 1)) ^ <*(f /. (len f))*>) ^ ((f /^ i) | (((len f) -' i) -' 1))) ^ <*(f /. i)*>) ^ {} by RFINSEQ:40 ;
hence Swap f,i,(len f) = (((f | (i -' 1)) ^ <*(f /. (len f))*>) ^ ((f /^ i) | (((len f) -' i) -' 1))) ^ <*(f /. i)*> by FINSEQ_1:47; :: thesis: verum