let R be Ring; :: thesis: for V being RightMod of R
for T, S being finite Subset of V holds Sum (T \/ S) = ((Sum T) + (Sum S)) - (Sum (T /\ S))
let V be RightMod of R; :: thesis: for T, S being finite Subset of V holds Sum (T \/ S) = ((Sum T) + (Sum S)) - (Sum (T /\ S))
let T, S be finite Subset of V; :: thesis: Sum (T \/ S) = ((Sum T) + (Sum S)) - (Sum (T /\ S))
set A = S \ T;
set B = T \ S;
set Z = (S \ T) \/ (T \ S);
set I = T /\ S;
(S \ T) \/ (T \ S) = T \+\ S ;
then A1: ( (S \ T) \/ (T \ S) misses T /\ S & ((S \ T) \/ (T \ S)) \/ (T /\ S) = T \/ S ) by XBOOLE_1:93, XBOOLE_1:103;
A2: ( S \ T misses T /\ S & (S \ T) \/ (T /\ S) = S ) by XBOOLE_1:51, XBOOLE_1:89;
A3: ( T \ S misses T /\ S & (T \ S) \/ (T /\ S) = T ) by XBOOLE_1:51, XBOOLE_1:89;
(Sum (T \/ S)) + (Sum (T /\ S)) = ((Sum ((S \ T) \/ (T \ S))) + (Sum (T /\ S))) + (Sum (T /\ S)) by A1, Th9
.= (((Sum (S \ T)) + (Sum (T \ S))) + (Sum (T /\ S))) + (Sum (T /\ S)) by Th9, XBOOLE_1:82
.= ((Sum (S \ T)) + ((Sum (T /\ S)) + (Sum (T \ S)))) + (Sum (T /\ S)) by RLVECT_1:def 6
.= ((Sum (S \ T)) + (Sum (T /\ S))) + ((Sum (T \ S)) + (Sum (T /\ S))) by RLVECT_1:def 6
.= (Sum S) + ((Sum (T \ S)) + (Sum (T /\ S))) by A2, Th9
.= (Sum T) + (Sum S) by A3, Th9 ;
hence Sum (T \/ S) = ((Sum T) + (Sum S)) - (Sum (T /\ S)) by RLSUB_2:78; :: thesis: verum