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 ) )

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 ) )

hence
( support b = {x} iff ( b = ({x},(b . x)) -bag & b . x <> 0 ) )
by UPROOTS:8; :: thesis: verumassume 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;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