let X be set ; :: thesis:
let p, q, r be real-valued ManySortedSet of X; :: thesis:
assume that
A1: (support p) /\ (support q) = {} and
A2: (support p) \/ (support q) = support r and
A3: p | (support p) = r | (support p) and
A4: q | (support q) = r | (support q) ; :: thesis:
for x being object st x in X holds
r . x = (p . x) + (q . x)

let x be object ; :: thesis:
assume x in X ; :: thesis:

suppose A5: x in (support p) \/ (support q) ; :: thesis:

per cases by A5, XBOOLE_0:def 3;

suppose A6: x in support p ; :: thesis:

then A7: not x in support q by A1, XBOOLE_0:def 4;
thus r . x = (r | (support p)) . x by A6, FUNCT_1:49
.= (p . x) + 0 by A3, A6, FUNCT_1:49
.= (p . x) + (q . x) by A7, PRE_POLY:def 7 ; :: thesis:

end;

suppose A8: x in support q ; :: thesis:

then A9: not x in support p by A1, XBOOLE_0:def 4;
thus r . x = (r | (support q)) . x by A8, FUNCT_1:49
.= 0 + (q . x) by A4, A8, FUNCT_1:49
.= (p . x) + (q . x) by A9, PRE_POLY:def 7 ; :: thesis:

end;

end;

end;

hence r . x = (p . x) + (q . x) ; :: thesis:

end;

suppose A10: not x in (support p) \/ (support q) ; :: thesis:

then A11: not x in support q by XBOOLE_0:def 3;
A12: not x in support p by A10, XBOOLE_0:def 3;
thus r . x = 0 by A2, A10, PRE_POLY:def 7
.= 0 + (q . x) by A11, PRE_POLY:def 7
.= (p . x) + (q . x) by A12, PRE_POLY:def 7 ; :: thesis:

end;

end;

end;

hence r = p + q by PRE_POLY:33; :: thesis: