let R be Ring; :: thesis: for V being RightMod of
for T, S being finite Subset of holds Sum (T \ S) = (Sum T) - (Sum (T /\ S))
let V be RightMod of ; :: thesis: for T, S being finite Subset of holds Sum (T \ S) = (Sum T) - (Sum (T /\ S))
let T, S be finite Subset of ; :: 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 Th12;
hence Sum (T \ S) = (Sum T) - (Sum (T /\ S)) by XBOOLE_1:22; :: thesis: verum