let F be Field; :: thesis: for B1, B2 being non zero bag of the carrier of F st B2 divides B1 & card B1 = 1 holds
B2 = B1
let B1, B2 be non zero bag of the carrier of F; :: thesis: ( B2 divides B1 & card B1 = 1 implies B2 = B1 )
assume A: ( B2 divides B1 & card B1 = 1 ) ; :: thesis: B2 = B1
then consider a1 being Element of F such that
B: B1 = Bag {a1} by bag2;
C: card B2 <= 1 by A, bag1;
support B2 <> {} by RING_5:24;
then card B2 >= 1 by RING_5:23, NAT_1:14;
then consider a2 being Element of F such that
D: B2 = Bag {a2} by C, XXREAL_0:1, bag2;
( B1 = ({a1},1) -bag & B2 = ({a2},1) -bag ) by B, D, RING_5:def 1;
then E: ( support B1 = {a1} & support B2 = {a2} ) by UPROOTS:8;
then a2 in support B2 by TARSKI:def 1;
then F: B2 . a2 <> 0 by PRE_POLY:def 7;

now :: thesis: not a1 <> a2

assume a1 <> a2 ; :: thesis: contradiction
then not a2 in support B1 by E, TARSKI:def 1;
then ( B1 . a2 = 0 & B2 . a2 > 0 ) by F, PRE_POLY:def 7;
hence contradiction by A, PRE_POLY:def 11; :: thesis: verum

end;

hence B2 = B1 by B, D; :: thesis: verum