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

let u be object ; :: thesis:
assume u in { [b9,(b + b9)] where b9 is Element of Bags n : b9 in Support p } ; :: thesis:
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:

end;

let x, y1, y2 be object ; :: thesis:
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:
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:

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;

let u be object ; :: thesis:
assume u in dom f ; :: thesis:
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:

end;

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

let u be object ; :: thesis:
assume u in Support (b *' p) ; :: thesis:
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:

end;

let u be object ; :: thesis:
assume A13: u in Support p ; :: thesis:
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:

end;