set f = { [b9,(b + b9)] where b9 is Element of Bags n : b9 in Support p } ;

A1: now

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

end;

now

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

end;

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

A6: 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
A7: [u,v] in f by RELAT_1:def 4;
consider b9 being Element of Bags n such that
A8: [u,v] = [b9,(b + b9)] and
A9: b9 in Support p by A7;
u = [b9,(b + b9)] `1 by A8, MCART_1:def 1
.= b9 by MCART_1:def 1 ;
hence u in Support p by A9; :: thesis: verum

end;

A10: Support (b *' p) c= { (b + b9) where b9 is Element of Bags n : b9 in Support p } by Lm10;

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 + b9) where b9 is Element of Bags n : b9 in Support p } by A10;
then consider b9 being Element of Bags n such that
A11: ( u = b + b9 & b9 in Support p ) ;
[b9,u] in f by A11;
hence u in rng f by RELAT_1:def 5; :: thesis: verum

end;

then A12: Support (b *' p) c= rng f by TARSKI:def 3;

now

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

end;

then dom f = Support p by A6, TARSKI:1;
then dom f is finite by POLYNOM1:def 4;
then rng f is finite by FINSET_1:8;
hence b *' p is finite-Support by A12, POLYNOM1:def 4; :: thesis: verum