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