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) - (Sum (T /\ S))

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

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

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

hence Sum (T \ S) = (Sum T) - (Sum (T /\ S)) by XBOOLE_1:22; :: thesis: verum

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

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

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

hence Sum (T \ S) = (Sum T) - (Sum (T /\ S)) by XBOOLE_1:22; :: thesis: verum