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 j in Seg (len f) by FINSEQ_1:1;
then A2: j in dom f by FINSEQ_1:def 3;
i in Seg (len f) by A1, FINSEQ_1:1;
then A3: i in dom f by FINSEQ_1:def 3;

now :: thesis: ( ( i = j & Sum (Swap (f,i,j)) = Sum f ) or ( i < j & Sum (Swap (f,i,j)) = Sum f ) or ( i > j & Sum (Swap (f,i,j)) = Sum f ) )

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:19; :: thesis: verum

end;

case A4: 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:27;
then A5: Sum (Swap (f,i,j)) = (Sum ((((f | (i -' 1)) ^ <*(f /. j)*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*(f /. i)*>)) + (Sum (f /^ j)) by RLVECT_1:41
.= ((Sum (((f | (i -' 1)) ^ <*(f /. j)*>) ^ ((f /^ i) | ((j -' i) -' 1)))) + (Sum <*(f /. i)*>)) + (Sum (f /^ j)) by RLVECT_1:41
.= (((Sum ((f | (i -' 1)) ^ <*(f /. j)*>)) + (Sum ((f /^ i) | ((j -' i) -' 1)))) + (Sum <*(f /. i)*>)) + (Sum (f /^ j)) by RLVECT_1:41
.= ((((Sum (f | (i -' 1))) + (Sum <*(f /. j)*>)) + (Sum ((f /^ i) | ((j -' i) -' 1)))) + (Sum <*(f /. i)*>)) + (Sum (f /^ j)) by RLVECT_1:41
.= ((((Sum (f | (i -' 1))) + (Sum <*(f /. j)*>)) + (Sum <*(f /. i)*>)) + (Sum ((f /^ i) | ((j -' i) -' 1)))) + (Sum (f /^ j)) by RLVECT_1:def 3
.= ((((Sum (f | (i -' 1))) + (Sum <*(f /. i)*>)) + (Sum <*(f /. j)*>)) + (Sum ((f /^ i) | ((j -' i) -' 1)))) + (Sum (f /^ j)) by RLVECT_1:def 3
.= (((Sum ((f | (i -' 1)) ^ <*(f /. i)*>)) + (Sum <*(f /. j)*>)) + (Sum ((f /^ i) | ((j -' i) -' 1)))) + (Sum (f /^ j)) by RLVECT_1:41
.= (((Sum ((f | (i -' 1)) ^ <*(f /. i)*>)) + (Sum ((f /^ i) | ((j -' i) -' 1)))) + (Sum <*(f /. j)*>)) + (Sum (f /^ j)) by RLVECT_1:def 3
.= ((Sum (((f | (i -' 1)) ^ <*(f /. i)*>) ^ ((f /^ i) | ((j -' i) -' 1)))) + (Sum <*(f /. j)*>)) + (Sum (f /^ j)) by RLVECT_1:41
.= (Sum ((((f | (i -' 1)) ^ <*(f /. i)*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*(f /. j)*>)) + (Sum (f /^ j)) by RLVECT_1:41
.= Sum (((((f | (i -' 1)) ^ <*(f /. i)*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*(f /. j)*>) ^ (f /^ j)) by RLVECT_1:41 ;
((((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 A3, PARTFUN1:def 6
.= ((((f | (i -' 1)) ^ <*(f . i)*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*(f . j)*>) ^ (f /^ j) by A2, PARTFUN1:def 6
.= f by A1, A4, FINSEQ_7:1 ;
hence Sum (Swap (f,i,j)) = Sum f by A5; :: thesis: verum

end;

case A6: 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:27;
then A7: Sum (Swap (f,j,i)) = (Sum ((((f | (j -' 1)) ^ <*(f /. i)*>) ^ ((f /^ j) | ((i -' j) -' 1))) ^ <*(f /. j)*>)) + (Sum (f /^ i)) by RLVECT_1:41
.= ((Sum (((f | (j -' 1)) ^ <*(f /. i)*>) ^ ((f /^ j) | ((i -' j) -' 1)))) + (Sum <*(f /. j)*>)) + (Sum (f /^ i)) by RLVECT_1:41
.= (((Sum ((f | (j -' 1)) ^ <*(f /. i)*>)) + (Sum ((f /^ j) | ((i -' j) -' 1)))) + (Sum <*(f /. j)*>)) + (Sum (f /^ i)) by RLVECT_1:41
.= ((((Sum (f | (j -' 1))) + (Sum <*(f /. i)*>)) + (Sum ((f /^ j) | ((i -' j) -' 1)))) + (Sum <*(f /. j)*>)) + (Sum (f /^ i)) by RLVECT_1:41
.= ((((Sum (f | (j -' 1))) + (Sum <*(f /. i)*>)) + (Sum <*(f /. j)*>)) + (Sum ((f /^ j) | ((i -' j) -' 1)))) + (Sum (f /^ i)) by RLVECT_1:def 3
.= ((((Sum (f | (j -' 1))) + (Sum <*(f /. j)*>)) + (Sum <*(f /. i)*>)) + (Sum ((f /^ j) | ((i -' j) -' 1)))) + (Sum (f /^ i)) by RLVECT_1:def 3
.= (((Sum ((f | (j -' 1)) ^ <*(f /. j)*>)) + (Sum <*(f /. i)*>)) + (Sum ((f /^ j) | ((i -' j) -' 1)))) + (Sum (f /^ i)) by RLVECT_1:41
.= (((Sum ((f | (j -' 1)) ^ <*(f /. j)*>)) + (Sum ((f /^ j) | ((i -' j) -' 1)))) + (Sum <*(f /. i)*>)) + (Sum (f /^ i)) by RLVECT_1:def 3
.= ((Sum (((f | (j -' 1)) ^ <*(f /. j)*>) ^ ((f /^ j) | ((i -' j) -' 1)))) + (Sum <*(f /. i)*>)) + (Sum (f /^ i)) by RLVECT_1:41
.= (Sum ((((f | (j -' 1)) ^ <*(f /. j)*>) ^ ((f /^ j) | ((i -' j) -' 1))) ^ <*(f /. i)*>)) + (Sum (f /^ i)) by RLVECT_1:41
.= Sum (((((f | (j -' 1)) ^ <*(f /. j)*>) ^ ((f /^ j) | ((i -' j) -' 1))) ^ <*(f /. i)*>) ^ (f /^ i)) by RLVECT_1:41 ;
((((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 6
.= ((((f | (j -' 1)) ^ <*(f . j)*>) ^ ((f /^ j) | ((i -' j) -' 1))) ^ <*(f . i)*>) ^ (f /^ i) by A3, PARTFUN1:def 6
.= f by A1, A6, FINSEQ_7:1 ;
hence Sum (Swap (f,i,j)) = Sum f by A7, FINSEQ_7:21; :: thesis: verum

end;

end;

end;

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

end;

end;