let X be set ; :: thesis: for S, T being finite Subset of X
for n being Element of NAT st S misses T holds
(S \/ T),n -bag = (S,n -bag ) + (T,n -bag )
let S, T be finite Subset of X; :: thesis: for n being Element of NAT st S misses T holds
(S \/ T),n -bag = (S,n -bag ) + (T,n -bag )
let n be Element of NAT ; :: thesis: ( S misses T implies (S \/ T),n -bag = (S,n -bag ) + (T,n -bag ) )
assume S misses T ; :: thesis: (S \/ T),n -bag = (S,n -bag ) + (T,n -bag )
then A1: S /\ T = {} by XBOOLE_0:def 7;

now

let i be set ; :: thesis: ( i in X implies ((S \/ T),n -bag ) . b₁ = ((S,n -bag ) + (T,n -bag )) . b₁ )
assume i in X ; :: thesis: ((S \/ T),n -bag ) . b₁ = ((S,n -bag ) + (T,n -bag )) . b₁

per cases ( not i in S \/ T or i in S or i in T ) by XBOOLE_0:def 3;

suppose A2: not i in S \/ T ; :: thesis: ((S \/ T),n -bag ) . b₁ = ((S,n -bag ) + (T,n -bag )) . b₁

then A3: ( not i in S & not i in T ) by XBOOLE_0:def 3;
thus ((S \/ T),n -bag ) . i = 0 by A2, Th8
.= ((S,n -bag ) . i) + 0 by A3, Th8
.= ((S,n -bag ) . i) + ((T,n -bag ) . i) by A3, Th8
.= ((S,n -bag ) + (T,n -bag )) . i by POLYNOM1:def 5 ; :: thesis: verum

end;

suppose A4: i in S ; :: thesis: ((S \/ T),n -bag ) . b₁ = ((S,n -bag ) + (T,n -bag )) . b₁

then A5: i in S \/ T by XBOOLE_0:def 3;
A6: not i in T by A1, A4, XBOOLE_0:def 4;
thus ((S \/ T),n -bag ) . i = n by A5, Th9
.= ((S,n -bag ) . i) + 0 by A4, Th9
.= ((S,n -bag ) . i) + ((T,n -bag ) . i) by A6, Th8
.= ((S,n -bag ) + (T,n -bag )) . i by POLYNOM1:def 5 ; :: thesis: verum

end;

suppose A7: i in T ; :: thesis: ((S \/ T),n -bag ) . b₁ = ((S,n -bag ) + (T,n -bag )) . b₁

then A8: i in S \/ T by XBOOLE_0:def 3;
A9: not i in S by A1, A7, XBOOLE_0:def 4;
thus ((S \/ T),n -bag ) . i = n by A8, Th9
.= ((T,n -bag ) . i) + 0 by A7, Th9
.= ((S,n -bag ) . i) + ((T,n -bag ) . i) by A9, Th8
.= ((S,n -bag ) + (T,n -bag )) . i by POLYNOM1:def 5 ; :: thesis: verum

end;

end;

end;

hence (S \/ T),n -bag = (S,n -bag ) + (T,n -bag ) by PBOOLE:3; :: thesis: verum