defpred S₁[ object ] means $1 in J;
deffunc H₁( object ) -> set = m . $1;
deffunc H₂( object ) -> Element of NAT = 0 ;
consider f being Function such that
A1: ( dom f = I & ( for x being object st x in I holds
( ( S₁[x] implies f . x = H₁(x) ) & ( not S₁[x] implies f . x = H₂(x) ) ) ) ) from PARTFUN1:sch 1();
rng f c= NAT

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in NAT )
assume x in rng f ; :: thesis: x in NAT
then consider i being object such that
A2: ( i in dom f & x = f . i ) by FUNCT_1:def 3;
( x = H₁(i) or x = H₂(i) ) by A1, A2;
hence x in NAT by ORDINAL1:def 12; :: thesis: verum

end;

then reconsider f = f as Function of I,NAT by A1, FUNCT_2:2;
f is finite-support

proof

support f c= support m

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in support f or x in support m )
assume x in support f ; :: thesis: x in support m
then A3: f . x <> 0 by PRE_POLY:def 7;
then x in dom f by FUNCT_1:def 2;
then f . x = m . x by A1, A3;
hence x in support m by A3, PRE_POLY:def 7; :: thesis: verum

end;

hence support f is finite ; :: according to PRE_POLY:def 8 :: thesis: verum

end;

then reconsider f = f as bag of I ;
take f ; :: thesis: for i being object st i in I holds
( ( i in J implies f . i = m . i ) & ( not i in J implies f . i = 0 ) )
thus for i being object st i in I holds
( ( i in J implies f . i = m . i ) & ( not i in J implies f . i = 0 ) ) by A1; :: thesis: verum