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 S)
let V be RightMod of R; :: 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 Th10;
then Sum (T \/ S) = ((Sum (T \ S)) + (Sum S)) - (0. V) by A1, Th5
.= (Sum (T \ S)) + (Sum S) by VECTSP_1:18 ;
hence Sum (T \ S) = (Sum (T \/ S)) - (Sum S) by RLSUB_2:61; :: thesis: verum