let n be set ; :: thesis: for b being bag of n st support b = {} holds
b = EmptyBag n
let b be bag of n; :: thesis: ( support b = {} implies b = EmptyBag n )
assume that
A1: support b = {} and
A2: b <> EmptyBag n ; :: thesis: contradiction
A3: dom b = n by PARTFUN1:def 2;
dom (EmptyBag n) = n by PARTFUN1:def 2;
then consider x being set such that
x in n and
A4: b . x <> (EmptyBag n) . x by A2, A3, FUNCT_1:2;
b . x <> 0 by A4, PRE_POLY:52;
hence contradiction by A1, PRE_POLY:def 7; :: thesis: verum