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) . 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 T by XBOOLE_0:def 3;
A4: not i in S by A2, XBOOLE_0:def 3;
thus (((S \/ T),n) -bag) . i = 0 by A2, Th3
.= (((S,n) -bag) . i) + 0 by A4, Th3
.= (((S,n) -bag) . i) + (((T,n) -bag) . i) by A3, Th3
.= (((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) . b₁ = (((S,n) -bag) + ((T,n) -bag)) . b₁

then A6: not i in T by A1, XBOOLE_0:def 4;
i in S \/ T by A5, XBOOLE_0:def 3;
hence (((S \/ T),n) -bag) . i = n by Th4
.= (((S,n) -bag) . i) + 0 by A5, Th4
.= (((S,n) -bag) . i) + (((T,n) -bag) . i) by A6, Th3
.= (((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) . b₁ = (((S,n) -bag) + ((T,n) -bag)) . b₁

then A8: not i in S by A1, XBOOLE_0:def 4;
i in S \/ T by A7, XBOOLE_0:def 3;
hence (((S \/ T),n) -bag) . i = n by Th4
.= (((T,n) -bag) . i) + 0 by A7, Th4
.= (((S,n) -bag) . i) + (((T,n) -bag) . i) by A8, Th3
.= (((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