A1: Support (b *' p) c= { (b + b') where b' is Element of Bags n : b' in Support p } by Lm10;
set f = { [b',(b + b')] where b' is Element of Bags n : b' in Support p } ;

A2: now

let u be set ; :: thesis: ( u in { [b',(b + b')] where b' is Element of Bags n : b' in Support p } implies ex y, z being set st u = [y,z] )
assume u in { [b',(b + b')] where b' is Element of Bags n : b' in Support p } ; :: thesis: ex y, z being set st u = [y,z]
then consider b' being Element of Bags n such that
A3: ( u = [b',(b + b')] & b' in Support p ) ;
thus ex y, z being set st u = [y,z] by A3; :: thesis: verum

end;

now

let x, y1, y2 be set ; :: thesis: ( [x,y1] in { [b',(b + b')] where b' is Element of Bags n : b' in Support p } & [x,y2] in { [b',(b + b')] where b' is Element of Bags n : b' in Support p } implies y1 = y2 )
assume A4: ( [x,y1] in { [b',(b + b')] where b' is Element of Bags n : b' in Support p } & [x,y2] in { [b',(b + b')] where b' is Element of Bags n : b' in Support p } ) ; :: thesis: y1 = y2
then consider b1 being Element of Bags n such that
A5: ( [x,y1] = [b1,(b + b1)] & b1 in Support p ) ;
consider b2 being Element of Bags n such that
A6: ( [x,y2] = [b2,(b + b2)] & b2 in Support p ) by A4;
b1 = [x,y1] `1 by A5, MCART_1:def 1
.= x by MCART_1:def 1
.= [b2,(b + b2)] `1 by A6, MCART_1:def 1
.= b2 by MCART_1:def 1 ;
hence y1 = [x,y2] `2 by A5, A6, MCART_1:def 2
.= y2 by MCART_1:def 2 ;
:: thesis: verum

end;

then reconsider f = { [b',(b + b')] where b' is Element of Bags n : b' in Support p } as Function by A2, FUNCT_1:def 1, RELAT_1:def 1;

A7: now

let u be set ; :: thesis: ( u in dom f implies u in Support p )
assume u in dom f ; :: thesis: u in Support p
then consider v being set such that
A8: [u,v] in f by RELAT_1:def 4;
consider b' being Element of Bags n such that
A9: ( [u,v] = [b',(b + b')] & b' in Support p ) by A8;
u = [b',(b + b')] `1 by A9, MCART_1:def 1
.= b' by MCART_1:def 1 ;
hence u in Support p by A9; :: thesis: verum

end;

now

let u be set ; :: thesis: ( u in Support p implies u in dom f )
assume A10: u in Support p ; :: thesis: u in dom f
then reconsider u' = u as Element of Bags n ;
[u',(b + u')] in { [b',(b + b')] where b' is Element of Bags n : b' in Support p } by A10;
hence u in dom f by RELAT_1:def 4; :: thesis: verum

end;

then dom f = Support p by A7, TARSKI:2;
then dom f is finite by POLYNOM1:def 10;
then A11: rng f is finite by FINSET_1:26;

now

let u be set ; :: thesis: ( u in Support (b *' p) implies u in rng f )
assume u in Support (b *' p) ; :: thesis: u in rng f
then u in { (b + b') where b' is Element of Bags n : b' in Support p } by A1;
then consider b' being Element of Bags n such that
A12: ( u = b + b' & b' in Support p ) ;
[b',u] in f by A12;
hence u in rng f by RELAT_1:def 5; :: thesis: verum

end;

then Support (b *' p) c= rng f by TARSKI:def 3;
then Support (b *' p) is finite by A11;
hence b *' p is finite-Support by POLYNOM1:def 10; :: thesis: verum