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 object ; :: 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 x9 = x as Element of NatMinor f ;
A1: dom x9 = X by FUNCT_2:92;
then A2: x9 is ManySortedSet of X by PARTFUN1:def 2, RELAT_1:def 18;
support x9 c= support f
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in support x9 or a in support f )
A3: support x9 c= dom x9 by Th36;
assume A4: a in support x9 ; :: thesis: a in support f
then x9 . a <> 0 by Def7;
then f . a <> 0 by A1, A2, A4, A3, Def14;
hence a in support f by Def7; :: thesis: verum
end;
then x is bag of X by A1, Def8, PARTFUN1:def 2, RELAT_1:def 18;
hence x in Bags X by Def12; :: thesis: verum