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))

Sum (T \/ S) = ((Sum T) + (Sum S)) - (Sum (T /\ S)) by Th13;

then (Sum T) + (Sum S) = (Sum (T /\ S)) + (Sum (T \/ S)) by RLSUB_2:61;

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))

Sum (T \/ S) = ((Sum T) + (Sum S)) - (Sum (T /\ S)) by Th13;

then (Sum T) + (Sum S) = (Sum (T /\ S)) + (Sum (T \/ S)) by RLSUB_2:61;

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