let L be non empty Abelian add-associative right_zeroed addLoopStr ; :: thesis: for f being FinSequence of L
for i, j being Element of NAT holds Sum (Swap f,i,j) = Sum f
let f be FinSequence of L; :: thesis: for i, j being Element of NAT holds Sum (Swap f,i,j) = Sum f
let i, j be Element of NAT ; :: thesis: Sum (Swap f,i,j) = Sum f

per cases ( not 1 <= i or not i <= len f or not 1 <= j or not j <= len f or ( 1 <= i & i <= len f & 1 <= j & j <= len f ) ) ;

suppose ( not 1 <= i or not i <= len f or not 1 <= j or not j <= len f ) ; :: thesis: Sum (Swap f,i,j) = Sum f

hence Sum (Swap f,i,j) = Sum f by FINSEQ_7:def 2; :: thesis: verum

end;

suppose A1: ( 1 <= i & i <= len f & 1 <= j & j <= len f ) ; :: thesis: Sum (Swap f,i,j) = Sum f

then ( i in Seg (len f) & j in Seg (len f) ) by FINSEQ_1:3;
then A2: ( i in dom f & j in dom f ) by FINSEQ_1:def 3;

now

per cases ( i = j or i < j or i > j ) by XXREAL_0:1;

case i = j ; :: thesis: Sum (Swap f,i,j) = Sum f

hence Sum (Swap f,i,j) = Sum f by FINSEQ_7:21; :: thesis: verum

end;

case A3: i < j ; :: thesis: Sum (Swap f,i,j) = Sum f

then Swap f,i,j = ((((f | (i -' 1)) ^ <*(f /. j)*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*(f /. i)*>) ^ (f /^ j) by A1, FINSEQ_7:29;
then A4: Sum (Swap f,i,j) = (Sum ((((f | (i -' 1)) ^ <*(f /. j)*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*(f /. i)*>)) + (Sum (f /^ j)) by RLVECT_1:58
.= ((Sum (((f | (i -' 1)) ^ <*(f /. j)*>) ^ ((f /^ i) | ((j -' i) -' 1)))) + (Sum <*(f /. i)*>)) + (Sum (f /^ j)) by RLVECT_1:58
.= (((Sum ((f | (i -' 1)) ^ <*(f /. j)*>)) + (Sum ((f /^ i) | ((j -' i) -' 1)))) + (Sum <*(f /. i)*>)) + (Sum (f /^ j)) by RLVECT_1:58
.= ((((Sum (f | (i -' 1))) + (Sum <*(f /. j)*>)) + (Sum ((f /^ i) | ((j -' i) -' 1)))) + (Sum <*(f /. i)*>)) + (Sum (f /^ j)) by RLVECT_1:58
.= ((((Sum (f | (i -' 1))) + (Sum <*(f /. j)*>)) + (Sum <*(f /. i)*>)) + (Sum ((f /^ i) | ((j -' i) -' 1)))) + (Sum (f /^ j)) by RLVECT_1:def 6
.= ((((Sum (f | (i -' 1))) + (Sum <*(f /. i)*>)) + (Sum <*(f /. j)*>)) + (Sum ((f /^ i) | ((j -' i) -' 1)))) + (Sum (f /^ j)) by RLVECT_1:def 6
.= (((Sum ((f | (i -' 1)) ^ <*(f /. i)*>)) + (Sum <*(f /. j)*>)) + (Sum ((f /^ i) | ((j -' i) -' 1)))) + (Sum (f /^ j)) by RLVECT_1:58
.= (((Sum ((f | (i -' 1)) ^ <*(f /. i)*>)) + (Sum ((f /^ i) | ((j -' i) -' 1)))) + (Sum <*(f /. j)*>)) + (Sum (f /^ j)) by RLVECT_1:def 6
.= ((Sum (((f | (i -' 1)) ^ <*(f /. i)*>) ^ ((f /^ i) | ((j -' i) -' 1)))) + (Sum <*(f /. j)*>)) + (Sum (f /^ j)) by RLVECT_1:58
.= (Sum ((((f | (i -' 1)) ^ <*(f /. i)*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*(f /. j)*>)) + (Sum (f /^ j)) by RLVECT_1:58
.= Sum (((((f | (i -' 1)) ^ <*(f /. i)*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*(f /. j)*>) ^ (f /^ j)) by RLVECT_1:58 ;
((((f | (i -' 1)) ^ <*(f /. i)*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*(f /. j)*>) ^ (f /^ j) = ((((f | (i -' 1)) ^ <*(f . i)*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*(f /. j)*>) ^ (f /^ j) by A2, PARTFUN1:def 8
.= ((((f | (i -' 1)) ^ <*(f . i)*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*(f . j)*>) ^ (f /^ j) by A2, PARTFUN1:def 8
.= f by A1, A3, FINSEQ_7:1 ;
hence Sum (Swap f,i,j) = Sum f by A4; :: thesis: verum

end;

case A5: i > j ; :: thesis: Sum (Swap f,i,j) = Sum f

then Swap f,j,i = ((((f | (j -' 1)) ^ <*(f /. i)*>) ^ ((f /^ j) | ((i -' j) -' 1))) ^ <*(f /. j)*>) ^ (f /^ i) by A1, FINSEQ_7:29;
then A6: Sum (Swap f,j,i) = (Sum ((((f | (j -' 1)) ^ <*(f /. i)*>) ^ ((f /^ j) | ((i -' j) -' 1))) ^ <*(f /. j)*>)) + (Sum (f /^ i)) by RLVECT_1:58
.= ((Sum (((f | (j -' 1)) ^ <*(f /. i)*>) ^ ((f /^ j) | ((i -' j) -' 1)))) + (Sum <*(f /. j)*>)) + (Sum (f /^ i)) by RLVECT_1:58
.= (((Sum ((f | (j -' 1)) ^ <*(f /. i)*>)) + (Sum ((f /^ j) | ((i -' j) -' 1)))) + (Sum <*(f /. j)*>)) + (Sum (f /^ i)) by RLVECT_1:58
.= ((((Sum (f | (j -' 1))) + (Sum <*(f /. i)*>)) + (Sum ((f /^ j) | ((i -' j) -' 1)))) + (Sum <*(f /. j)*>)) + (Sum (f /^ i)) by RLVECT_1:58
.= ((((Sum (f | (j -' 1))) + (Sum <*(f /. i)*>)) + (Sum <*(f /. j)*>)) + (Sum ((f /^ j) | ((i -' j) -' 1)))) + (Sum (f /^ i)) by RLVECT_1:def 6
.= ((((Sum (f | (j -' 1))) + (Sum <*(f /. j)*>)) + (Sum <*(f /. i)*>)) + (Sum ((f /^ j) | ((i -' j) -' 1)))) + (Sum (f /^ i)) by RLVECT_1:def 6
.= (((Sum ((f | (j -' 1)) ^ <*(f /. j)*>)) + (Sum <*(f /. i)*>)) + (Sum ((f /^ j) | ((i -' j) -' 1)))) + (Sum (f /^ i)) by RLVECT_1:58
.= (((Sum ((f | (j -' 1)) ^ <*(f /. j)*>)) + (Sum ((f /^ j) | ((i -' j) -' 1)))) + (Sum <*(f /. i)*>)) + (Sum (f /^ i)) by RLVECT_1:def 6
.= ((Sum (((f | (j -' 1)) ^ <*(f /. j)*>) ^ ((f /^ j) | ((i -' j) -' 1)))) + (Sum <*(f /. i)*>)) + (Sum (f /^ i)) by RLVECT_1:58
.= (Sum ((((f | (j -' 1)) ^ <*(f /. j)*>) ^ ((f /^ j) | ((i -' j) -' 1))) ^ <*(f /. i)*>)) + (Sum (f /^ i)) by RLVECT_1:58
.= Sum (((((f | (j -' 1)) ^ <*(f /. j)*>) ^ ((f /^ j) | ((i -' j) -' 1))) ^ <*(f /. i)*>) ^ (f /^ i)) by RLVECT_1:58 ;
((((f | (j -' 1)) ^ <*(f /. j)*>) ^ ((f /^ j) | ((i -' j) -' 1))) ^ <*(f /. i)*>) ^ (f /^ i) = ((((f | (j -' 1)) ^ <*(f . j)*>) ^ ((f /^ j) | ((i -' j) -' 1))) ^ <*(f /. i)*>) ^ (f /^ i) by A2, PARTFUN1:def 8
.= ((((f | (j -' 1)) ^ <*(f . j)*>) ^ ((f /^ j) | ((i -' j) -' 1))) ^ <*(f . i)*>) ^ (f /^ i) by A2, PARTFUN1:def 8
.= f by A1, A5, FINSEQ_7:1 ;
hence Sum (Swap f,i,j) = Sum f by A6, FINSEQ_7:23; :: thesis: verum

end;

end;

end;

hence Sum (Swap f,i,j) = Sum f ; :: thesis: verum

end;

end;