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 Th27
.= ((((f | (i -' 1)) ^ <*(f /. (len f))*>) ^ ((f /^ i) | (((len f) -' i) -' 1))) ^ <*(f /. i)*>) ^ {} by RFINSEQ:27 ;
hence Swap (f,i,(len f)) = (((f | (i -' 1)) ^ <*(f /. (len f))*>) ^ ((f /^ i) | (((len f) -' i) -' 1))) ^ <*(f /. i)*> by FINSEQ_1:34; :: thesis: verum