let X be set ; :: thesis: for b being bag of X st support b = {} holds
b = EmptyBag X
let b be bag of X; :: thesis: ( support b = {} implies b = EmptyBag X )
A1: X = dom (EmptyBag X) by PARTFUN1:def 2;
assume A2: support b = {} ; :: thesis: b = EmptyBag X
A3: for u being set st u in X holds
b . u = (EmptyBag X) . u

proof

let u be set ; :: thesis: ( u in X implies b . u = (EmptyBag X) . u )
assume u in X ; :: thesis: b . u = (EmptyBag X) . u
b . u = 0 by A2, PRE_POLY:def 7;
hence b . u = (EmptyBag X) . u by PRE_POLY:52; :: thesis: verum

end;

X = dom b by PARTFUN1:def 2;
hence b = EmptyBag X by A1, A3, FUNCT_1:2; :: thesis: verum