let F be domRing; :: thesis: for B1 being bag of the carrier of F holds
( card B1 = 1 iff ex a being Element of F st B1 = Bag {a} )
let B1 be bag of the carrier of F; :: thesis: ( card B1 = 1 iff ex a being Element of F st B1 = Bag {a} )

A: now :: thesis: ( card B1 = 1 implies ex a being Element of F st B1 = Bag {a} )

assume B: card B1 = 1 ; :: thesis: ex a being Element of F st B1 = Bag {a}
then C: support B1 <> {} by RING_5:23;
set a = the Element of support B1;
G: the Element of support B1 in support B1 by C;
then reconsider a = the Element of support B1 as Element of F ;
B1 . a <> 0 by C, PRE_POLY:def 7;
then E: ( B1 . a >= 1 & B1 . a <= 1 ) by B, bag2a, NAT_1:14;

now :: thesis: for o being object st o in support B1 holds
o in {a}

let o be object ; :: thesis: ( o in support B1 implies o in {a} )
assume o in support B1 ; :: thesis: o in {a}
then B1 . o <> 0 by PRE_POLY:def 7;
then o = a by B, E, bag2b, XXREAL_0:1;
hence o in {a} by TARSKI:def 1; :: thesis: verum

end;

then F: support B1 c= {a} ;
{a} c= support B1 by G, TARSKI:def 1;
then D: support B1 = {a} by F;
card {a} = 1 by CARD_2:42;
then B1 = ({a},1) -bag by B, D, UPROOTS:13
.= Bag {a} by RING_5:def 1 ;
hence ex a being Element of F st B1 = Bag {a} ; :: thesis: verum

end;

now :: thesis: ( ex a being Element of F st B1 = Bag {a} implies card B1 = 1 )

assume ex a being Element of F st B1 = Bag {a} ; :: thesis: card B1 = 1
then consider a being Element of F such that
A: B1 = Bag {a} ;
B1 = ({a},1) -bag by A, RING_5:def 1;
then card B1 = card {a} by UPROOTS:13;
hence card B1 = 1 by CARD_2:42; :: thesis: verum

end;

hence ( card B1 = 1 iff ex a being Element of F st B1 = Bag {a} ) by A; :: thesis: verum