let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; :: thesis: for S, T being finite Subset of V holds Sum (T \ S) = (Sum (T \/ S)) - (Sum S)

let S, T be finite Subset of V; :: thesis: Sum (T \ S) = (Sum (T \/ S)) - (Sum S)

T \ S misses S by XBOOLE_1:79;

then A1: (T \ S) /\ S = {} V ;

(T \ S) \/ S = T \/ S by XBOOLE_1:39;

then Sum (T \/ S) = ((Sum (T \ S)) + (Sum S)) - (Sum ((T \ S) /\ S)) by Th13;

then Sum (T \/ S) = ((Sum (T \ S)) + (Sum S)) - (0. V) by A1, Th8

.= (Sum (T \ S)) + (Sum S) ;

hence Sum (T \ S) = (Sum (T \/ S)) - (Sum S) by RLSUB_2:61; :: thesis: verum

let S, T be finite Subset of V; :: thesis: Sum (T \ S) = (Sum (T \/ S)) - (Sum S)

T \ S misses S by XBOOLE_1:79;

then A1: (T \ S) /\ S = {} V ;

(T \ S) \/ S = T \/ S by XBOOLE_1:39;

then Sum (T \/ S) = ((Sum (T \ S)) + (Sum S)) - (Sum ((T \ S) /\ S)) by Th13;

then Sum (T \/ S) = ((Sum (T \ S)) + (Sum S)) - (0. V) by A1, Th8

.= (Sum (T \ S)) + (Sum S) ;

hence Sum (T \ S) = (Sum (T \/ S)) - (Sum S) by RLSUB_2:61; :: thesis: verum