let Z be non empty set ; :: thesis: for B1, B2 being bag of Z st B2 divides B1 & B1 -' B2 is zero holds
B2 = B1
let B1, B2 be bag of Z; :: thesis: ( B2 divides B1 & B1 -' B2 is zero implies B2 = B1 )
assume A: ( B2 divides B1 & B1 -' B2 is zero ) ; :: thesis: B2 = B1

now :: thesis: not B2 <> B1

assume B2 <> B1 ; :: thesis: contradiction
then consider i being object such that
C: ( i in Z & B2 . i <> B1 . i ) by PBOOLE:3;
reconsider n = (B1 . i) - (B2 . i) as Element of NAT by INT_1:5, A, PRE_POLY:def 11;
n <> 0 by C;
then (B1 . i) -' (B2 . i) > 0 by XREAL_0:def 2;
then (B1 -' B2) . i > 0 by PRE_POLY:def 6;
then i in support (B1 -' B2) by PRE_POLY:def 7;
hence contradiction by A, RING_5:24; :: thesis: verum

end;

hence B2 = B1 ; :: thesis: verum