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

let S, T 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;

A1: (S \ T) \/ (T /\ S) = S by XBOOLE_1:51;

A2: (T \ S) \/ (T /\ S) = T by XBOOLE_1:51;

A3: (S \ T) \/ (T \ S) = T \+\ S ;

then ((S \ T) \/ (T \ S)) \/ (T /\ S) = T \/ S by XBOOLE_1:93;

then (Sum (T \/ S)) + (Sum (T /\ S)) = ((Sum ((S \ T) \/ (T \ S))) + (Sum (T /\ S))) + (Sum (T /\ S)) by A3, Th12, XBOOLE_1:103

.= (((Sum (S \ T)) + (Sum (T \ S))) + (Sum (T /\ S))) + (Sum (T /\ S)) by Th12, XBOOLE_1:82

.= ((Sum (S \ T)) + ((Sum (T /\ S)) + (Sum (T \ S)))) + (Sum (T /\ S)) by RLVECT_1:def 3

.= ((Sum (S \ T)) + (Sum (T /\ S))) + ((Sum (T \ S)) + (Sum (T /\ S))) by RLVECT_1:def 3

.= (Sum S) + ((Sum (T \ S)) + (Sum (T /\ S))) by A1, Th12, XBOOLE_1:89

.= (Sum T) + (Sum S) by A2, Th12, XBOOLE_1:89 ;

hence Sum (T \/ S) = ((Sum T) + (Sum S)) - (Sum (T /\ S)) by RLSUB_2:61; :: thesis: verum

let S, T 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;

A1: (S \ T) \/ (T /\ S) = S by XBOOLE_1:51;

A2: (T \ S) \/ (T /\ S) = T by XBOOLE_1:51;

A3: (S \ T) \/ (T \ S) = T \+\ S ;

then ((S \ T) \/ (T \ S)) \/ (T /\ S) = T \/ S by XBOOLE_1:93;

then (Sum (T \/ S)) + (Sum (T /\ S)) = ((Sum ((S \ T) \/ (T \ S))) + (Sum (T /\ S))) + (Sum (T /\ S)) by A3, Th12, XBOOLE_1:103

.= (((Sum (S \ T)) + (Sum (T \ S))) + (Sum (T /\ S))) + (Sum (T /\ S)) by Th12, XBOOLE_1:82

.= ((Sum (S \ T)) + ((Sum (T /\ S)) + (Sum (T \ S)))) + (Sum (T /\ S)) by RLVECT_1:def 3

.= ((Sum (S \ T)) + (Sum (T /\ S))) + ((Sum (T \ S)) + (Sum (T /\ S))) by RLVECT_1:def 3

.= (Sum S) + ((Sum (T \ S)) + (Sum (T /\ S))) by A1, Th12, XBOOLE_1:89

.= (Sum T) + (Sum S) by A2, Th12, XBOOLE_1:89 ;

hence Sum (T \/ S) = ((Sum T) + (Sum S)) - (Sum (T /\ S)) by RLSUB_2:61; :: thesis: verum