let X be non empty set ; :: thesis: for b being non empty bag of X
for x being Element of X holds
( support b = {x} iff ( b = ({x},(b . x)) -bag & b . x <> 0 ) )
let b be non empty bag of X; :: thesis: for x being Element of X holds
( support b = {x} iff ( b = ({x},(b . x)) -bag & b . x <> 0 ) )
let x be Element of X; :: thesis: ( support b = {x} iff ( b = ({x},(b . x)) -bag & b . x <> 0 ) )
now :: thesis: ( support b = {x} implies ( b = ({x},(b . x)) -bag & b . x <> 0 ) )
assume AS: support b = {x} ; :: thesis: ( b = ({x},(b . x)) -bag & b . x <> 0 )
then x in support b by TARSKI:def 1;
hence ( b = ({x},(b . x)) -bag & b . x <> 0 ) by AS, bb7a, PRE_POLY:def 7; :: thesis: verum
end;
hence ( support b = {x} iff ( b = ({x},(b . x)) -bag & b . x <> 0 ) ) by UPROOTS:8; :: thesis: verum