let X be set ; :: thesis: 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
let p, q, r be real-valued ManySortedSet of X; :: thesis: ( (support p) /\ (support q) = {} & (support p) \/ (support q) = support r & p | (support p) = r | (support p) & q | (support q) = r | (support q) implies p + q = r )
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: p + q = r
for x being object st x in X holds
r . x = (p . x) + (q . x)

proof

let x be object ; :: thesis: ( x in X implies r . x = (p . x) + (q . x) )
assume x in X ; :: thesis: r . x = (p . x) + (q . x)

per cases ( x in (support p) \/ (support q) or not x in (support p) \/ (support q) ) ;

suppose A5: x in (support p) \/ (support q) ; :: thesis: r . x = (p . x) + (q . x)

now :: thesis: r . x = (p . x) + (q . x)

per cases ( x in support p or x in support q ) by A5, XBOOLE_0:def 3;

suppose A6: x in support p ; :: thesis: r . x = (p . x) + (q . x)

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: verum

end;

suppose A8: x in support q ; :: thesis: r . x = (p . x) + (q . x)

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: verum

end;

end;

end;

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

end;

suppose A10: not x in (support p) \/ (support q) ; :: thesis: r . x = (p . x) + (q . x)

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: verum

end;

end;

end;

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