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 :: thesis: for i being object st i in X holds
(((S \/ T),n) -bag) . i = (((S,n) -bag) + ((T,n) -bag)) . i
let i be object ; :: thesis: ( i in X implies (((S \/ T),n) -bag) . b1 = (((S,n) -bag) + ((T,n) -bag)) . b1 )
assume i in X ; :: thesis: (((S \/ T),n) -bag) . b1 = (((S,n) -bag) + ((T,n) -bag)) . b1
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) . b1 = (((S,n) -bag) + ((T,n) -bag)) . b1
then A3: not i in T by XBOOLE_0:def 3;
A4: not i in S by ;
thus (((S \/ T),n) -bag) . i = 0 by
.= (((S,n) -bag) . i) + 0 by
.= (((S,n) -bag) . i) + (((T,n) -bag) . i) by
.= (((S,n) -bag) + ((T,n) -bag)) . i by PRE_POLY:def 5 ; :: thesis: verum
end;
suppose A5: i in S ; :: thesis: (((S \/ T),n) -bag) . b1 = (((S,n) -bag) + ((T,n) -bag)) . b1
then A6: not i in T by ;
i in S \/ T by ;
hence (((S \/ T),n) -bag) . i = n by Th4
.= (((S,n) -bag) . i) + 0 by
.= (((S,n) -bag) . i) + (((T,n) -bag) . i) by
.= (((S,n) -bag) + ((T,n) -bag)) . i by PRE_POLY:def 5 ;
:: thesis: verum
end;
suppose A7: i in T ; :: thesis: (((S \/ T),n) -bag) . b1 = (((S,n) -bag) + ((T,n) -bag)) . b1
then A8: not i in S by ;
i in S \/ T by ;
hence (((S \/ T),n) -bag) . i = n by Th4
.= (((T,n) -bag) . i) + 0 by
.= (((S,n) -bag) . i) + (((T,n) -bag) . i) by
.= (((S,n) -bag) + ((T,n) -bag)) . i by PRE_POLY:def 5 ;
:: thesis: verum
end;
end;
end;
hence ((S \/ T),n) -bag = ((S,n) -bag) + ((T,n) -bag) by PBOOLE:3; :: thesis: verum