let X be set ; :: thesis:
let b1, b2 be natural-valued ManySortedSet of X; :: thesis:

let x be object ; :: thesis:

hereby :: thesis:

assume x in (support b1) \/ (support b2) ; :: thesis:
then ( x in support b1 or x in support b2 ) by XBOOLE_0:def 3;
then ( b1 . x <> 0 or b2 . x <> 0 ) by Def7;
then (b1 . x) + (b2 . x) <> 0 ;
hence (b1 + b2) . x <> 0 by Def5; :: thesis:

end;

assume A1: (b1 + b2) . x <> 0 ; :: thesis:
assume A2: not x in (support b1) \/ (support b2) ; :: thesis:
then not x in support b1 by XBOOLE_0:def 3;
then A3: b1 . x = 0 by Def7;
not x in support b2 by A2, XBOOLE_0:def 3;
then (b1 . x) + (b2 . x) = 0 by A3, Def7;
hence contradiction by A1, Def5; :: thesis:

end;

hence support (b1 + b2) = (support b1) \/ (support b2) by Def7; :: thesis: