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

A1: now :: thesis: for u being object st u in { [b9,(b + b9)] where b9 is Element of Bags n : b9 in Support p } holds
ex y, z being object st u = [y,z]

let u be object ; :: thesis: ( u in { [b9,(b + b9)] where b9 is Element of Bags n : b9 in Support p } implies ex y, z being object 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 object 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 object st u = [y,z] ; :: thesis: verum

end;

now :: thesis: for x, y1, y2 being object st [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 } holds
y1 = y2

let x, y1, y2 be object ; :: 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 by A5, XTUPLE_0:1
.= b2 by A4, XTUPLE_0:1 ;
hence y1 = y2 by A5, A4, XTUPLE_0:1; :: 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 :: thesis: for u being object st u in dom f holds
u in Support p

let u be object ; :: thesis: ( u in dom f implies u in Support p )
assume u in dom f ; :: thesis: u in Support p
then consider v being object such that
A7: [u,v] in f by XTUPLE_0:def 12;
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 by A8, XTUPLE_0: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 :: thesis: for u being object st u in Support (b *' p) holds
u in rng f

let u be object ; :: 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 XTUPLE_0:def 13; :: thesis: verum

end;

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

now :: thesis: for u being object st u in Support p holds
u in dom f

let u be object ; :: 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 XTUPLE_0:def 12; :: thesis: verum

end;

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