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,1,i) = ((<*(f /. i)*> ^ ((f /^ 1) | (i -' 2))) ^ <*(f /. 1)*>) ^ (f /^ i)
let f be FinSequence of D; :: thesis: for i being Nat st 1 < i & i <= len f holds
Swap (f,1,i) = ((<*(f /. i)*> ^ ((f /^ 1) | (i -' 2))) ^ <*(f /. 1)*>) ^ (f /^ i)
let i be Nat; :: thesis: ( 1 < i & i <= len f implies Swap (f,1,i) = ((<*(f /. i)*> ^ ((f /^ 1) | (i -' 2))) ^ <*(f /. 1)*>) ^ (f /^ i) )
assume ( 1 < i & i <= len f ) ; :: thesis: Swap (f,1,i) = ((<*(f /. i)*> ^ ((f /^ 1) | (i -' 2))) ^ <*(f /. 1)*>) ^ (f /^ i)
then Swap (f,1,i) = ((((f | (1 -' 1)) ^ <*(f /. i)*>) ^ ((f /^ 1) | ((i -' 1) -' 1))) ^ <*(f /. 1)*>) ^ (f /^ i) by Th27
.= ((((f | 0) ^ <*(f /. i)*>) ^ ((f /^ 1) | ((i -' 1) -' 1))) ^ <*(f /. 1)*>) ^ (f /^ i) by XREAL_1:232
.= ((<*(f /. i)*> ^ ((f /^ 1) | ((i -' 1) -' 1))) ^ <*(f /. 1)*>) ^ (f /^ i) by FINSEQ_1:34 ;
hence Swap (f,1,i) = ((<*(f /. i)*> ^ ((f /^ 1) | (i -' 2))) ^ <*(f /. 1)*>) ^ (f /^ i) by NAT_D:45; :: thesis: verum