let n be set ; :: thesis: for b1, b2 being bag of n st b1 divides b2 & b2 -' b1 = EmptyBag n holds
b2 = b1
let b1, b2 be bag of n; :: thesis: ( b1 divides b2 & b2 -' b1 = EmptyBag n implies b2 = b1 )
assume that
A1: b1 divides b2 and
A2: b2 -' b1 = EmptyBag n ; :: thesis: b2 = b1
now :: thesis: for k being object st k in n holds
b2 . k = b1 . k
let k be object ; :: thesis: ( k in n implies b2 . k = b1 . k )
assume k in n ; :: thesis: b2 . k = b1 . k
0 = (b2 -' b1) . k by A2
.= (b2 . k) -' (b1 . k) by Def6 ;
then A3: b2 . k <= b1 . k by NAT_D:36;
b1 . k <= b2 . k by A1;
hence b2 . k = b1 . k by A3, XXREAL_0:1; :: thesis: verum
end;
hence b2 = b1 ; :: thesis: verum