let R be Ring; :: thesis: for V being RightMod of R
for S, T being finite Subset of V holds Sum (T \+\ S) = (Sum (T \/ S)) - (Sum (T /\ S))
let V be RightMod of R; :: thesis: for S, T being finite Subset of V holds Sum (T \+\ S) = (Sum (T \/ S)) - (Sum (T /\ S))
let S, T be finite Subset of V; :: thesis: Sum (T \+\ S) = (Sum (T \/ S)) - (Sum (T /\ S))
T \+\ S = (T \/ S) \ (T /\ S) by XBOOLE_1:101;
hence Sum (T \+\ S) = (Sum (T \/ S)) - (Sum ((T \/ S) /\ (T /\ S))) by Th13
.= (Sum (T \/ S)) - (Sum (((T \/ S) /\ T) /\ S)) by XBOOLE_1:16
.= (Sum (T \/ S)) - (Sum (T /\ S)) by XBOOLE_1:21 ;
:: thesis: verum