theorem Th2: :: INT_7:2

for X being set
for p, q, r being real-valued ManySortedSet of X st (support p) /\ (support q) = {} & (support p) \/ (support q) = support r & p | (support p) = r | (support p) & q | (support q) = r | (support q) holds
p + q = r