let X be set ; :: thesis: X --> 0 is bag of X
set f = X --> 0;
A1: dom (X --> 0) = X by FUNCOP_1:19;
support (X --> 0) = {}

proof

assume not support (X --> 0) = {} ; :: thesis: contradiction
then consider x being set such that
A2: x in support (X --> 0) by XBOOLE_0:def 1;
support (X --> 0) c= dom (X --> 0) by Th41;
then (X --> 0) . x = 0 by A1, A2, FUNCOP_1:13;
hence contradiction by A2, Def7; :: thesis: verum

end;

hence X --> 0 is bag of X by Def8; :: thesis: verum