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 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, Th8
.= ((S,n -bag ) . i) + 0 by A4, Th8
.= ((S,n -bag ) . i) + ((T,n -bag ) . i) by A3, Th8
.= ((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 Th9
.= ((S,n -bag ) . i) + 0 by A5, Th9
.= ((S,n -bag ) . i) + ((T,n -bag ) . i) by A6, Th8
.= ((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 Th9
.= ((T,n -bag ) . i) + 0 by A7, Th9
.= ((S,n -bag ) . i) + ((T,n -bag ) . i) by A8, Th8
.= ((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