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

proof

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

end;

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