let I, J be set ; :: thesis: for m being bag of I holds (m | J) + (m | (I \ J)) = m
let m be bag of I; :: thesis: (m | J) + (m | (I \ J)) = m
let i be object ; :: according to PBOOLE:def 10 :: thesis: ( not i in I or ((m | J) + (m | (I \ J))) . i = m . i )
assume A1: i in I ; :: thesis: ((m | J) + (m | (I \ J))) . i = m . i
A3: ((m | J) + (m | (I \ J))) . i = ((m | J) . i) + ((m | (I \ J)) . i) by PRE_POLY:def 5;

per cases ( i in J or not i in J ) ;

suppose A2: i in J ; :: thesis: ((m | J) + (m | (I \ J))) . i = m . i

then not i in I \ J by XBOOLE_0:def 5;
then ( (m | J) . i = m . i & (m | (I \ J)) . i = 0 ) by A1, A2, BAR;
hence ((m | J) + (m | (I \ J))) . i = m . i by A3; :: thesis: verum

end;

suppose A2: not i in J ; :: thesis: ((m | J) + (m | (I \ J))) . i = m . i

then i in I \ J by A1, XBOOLE_0:def 5;
then ( (m | J) . i = 0 & (m | (I \ J)) . i = m . i ) by A2, BAR;
hence ((m | J) + (m | (I \ J))) . i = m . i by A3; :: thesis: verum

end;

end;