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