let X be set ; :: thesis: for b1, b2 being natural-valued ManySortedSet of X holds support (b1 + b2) = (support b1) \/ (support b2)
let b1, b2 be natural-valued ManySortedSet of X; :: thesis: support (b1 + b2) = (support b1) \/ (support b2)

now

let x be set ; :: thesis: ( ( x in (support b1) \/ (support b2) implies (b1 + b2) . x <> 0 ) & ( (b1 + b2) . x <> 0 implies x in (support b1) \/ (support b2) ) )

hereby :: thesis: ( (b1 + b2) . x <> 0 implies x in (support b1) \/ (support b2) )

assume x in (support b1) \/ (support b2) ; :: thesis: (b1 + b2) . x <> 0
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: verum

end;

assume A1: (b1 + b2) . x <> 0 ; :: thesis: x in (support b1) \/ (support b2)
assume A2: not x in (support b1) \/ (support b2) ; :: thesis: contradiction
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: verum

end;

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