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 \/ 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 Th16

.= (Sum (T \/ S)) - (Sum (((T \/ S) /\ T) /\ S)) by XBOOLE_1:16

.= (Sum (T \/ S)) - (Sum (T /\ S)) by XBOOLE_1:21 ;

:: thesis: verum

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 Th16

.= (Sum (T \/ S)) - (Sum (((T \/ S) /\ T) /\ S)) by XBOOLE_1:16

.= (Sum (T \/ S)) - (Sum (T /\ S)) by XBOOLE_1:21 ;

:: thesis: verum