let X be set ; :: thesis: for f being finite-support Function of X,NAT holds NatMinor f c= Bags X
let f be finite-support Function of X,NAT ; :: thesis: NatMinor f c= Bags X
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in NatMinor f or x in Bags X )
assume x in NatMinor f ; :: thesis: x in Bags X
then reconsider x' = x as Element of NatMinor f ;
A1: dom x' = X by FUNCT_2:169;
then A2: x' is ManySortedSet of by PARTFUN1:def 4, RELAT_1:def 18;
support x' c= support f

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in support x' or a in support f )
assume A3: a in support x' ; :: thesis: a in support f
then x' . a <> 0 by Def7;
then A4: 0 < x' . a ;
support x' c= dom x' by Th41;
then f . a <> 0 by A1, A2, A3, A4, Def17;
hence a in support f by Def7; :: thesis: verum

end;

then support x' is finite ;
then x is bag of by A1, Def8, PARTFUN1:def 4, RELAT_1:def 18;
hence x in Bags X by Def14; :: thesis: verum