let n be set ; :: thesis: for b1, b2 being bag of n holds
( b1 divides b2 iff ex b being bag of n st b2 = b1 + b )
let b1, b2 be bag of n; :: thesis: ( b1 divides b2 iff ex b being bag of n st b2 = b1 + b )

now :: thesis: ( b1 divides b2 implies ex b being bag of n st b2 = b1 + b )

assume A1: b1 divides b2 ; :: thesis: ex b being bag of n st b2 = b1 + b

A2: now :: thesis: for k being object holds 0 <= (b2 . k) - (b1 . k)

let k be object ; :: thesis: 0 <= (b2 . k) - (b1 . k)
b1 . k <= b2 . k by A1, PRE_POLY:def 11;
then (b1 . k) - (b1 . k) <= (b2 . k) - (b1 . k) by XREAL_1:9;
hence 0 <= (b2 . k) - (b1 . k) ; :: thesis: verum

end;

now :: thesis: ( ( n = {} & ex b being bag of n st b2 = b1 + b ) or ( n <> {} & ex b, b being bag of n st b2 = b1 + b ) )

per cases ( n = {} or n <> {} ) ;

case A3: n = {} ; :: thesis: ex b being bag of n st b2 = b1 + b

then b1 + (EmptyBag n) = EmptyBag n by POLYNOM7:3
.= b2 by A3, POLYNOM7:3 ;
hence ex b being bag of n st b2 = b1 + b ; :: thesis: verum

end;

case n <> {} ; :: thesis: ex b, b being bag of n st b2 = b1 + b

then reconsider n9 = n as non empty set ;
set b = { [k,((b2 . k) -' (b1 . k))] where k is Element of n9 : verum } ;

A4: now :: thesis: for x being object st x in { [k,((b2 . k) -' (b1 . k))] where k is Element of n9 : verum } holds
ex y, z being object st x = [y,z]

let x be object ; :: thesis: ( x in { [k,((b2 . k) -' (b1 . k))] where k is Element of n9 : verum } implies ex y, z being object st x = [y,z] )
assume x in { [k,((b2 . k) -' (b1 . k))] where k is Element of n9 : verum } ; :: thesis: ex y, z being object st x = [y,z]
then ex k being Element of n9 st x = [k,((b2 . k) -' (b1 . k))] ;
hence ex y, z being object st x = [y,z] ; :: thesis: verum

end;

now :: thesis: for x, y1, y2 being object st [x,y1] in { [k,((b2 . k) -' (b1 . k))] where k is Element of n9 : verum } & [x,y2] in { [k,((b2 . k) -' (b1 . k))] where k is Element of n9 : verum } holds
y1 = y2

let x, y1, y2 be object ; :: thesis: ( [x,y1] in { [k,((b2 . k) -' (b1 . k))] where k is Element of n9 : verum } & [x,y2] in { [k,((b2 . k) -' (b1 . k))] where k is Element of n9 : verum } implies y1 = y2 )
assume that
A5: [x,y1] in { [k,((b2 . k) -' (b1 . k))] where k is Element of n9 : verum } and
A6: [x,y2] in { [k,((b2 . k) -' (b1 . k))] where k is Element of n9 : verum } ; :: thesis: y1 = y2
consider k being Element of n9 such that
A7: [x,y1] = [k,((b2 . k) -' (b1 . k))] by A5;
consider k9 being Element of n9 such that
A8: [x,y2] = [k9,((b2 . k9) -' (b1 . k9))] by A6;
k = x by A7, XTUPLE_0:1
.= k9 by A8, XTUPLE_0:1 ;
hence y1 = y2 by A7, A8, XTUPLE_0:1; :: thesis: verum

end;

then reconsider b = { [k,((b2 . k) -' (b1 . k))] where k is Element of n9 : verum } as Function by A4, FUNCT_1:def 1, RELAT_1:def 1;

A9: now :: thesis: for x being object st x in dom b holds
x in n9

let x be object ; :: thesis: ( x in dom b implies x in n9 )
assume x in dom b ; :: thesis: x in n9
then consider y being object such that
A10: [x,y] in b by XTUPLE_0:def 12;
consider k being Element of n9 such that
A11: [x,y] = [k,((b2 . k) -' (b1 . k))] by A10;
x = k by A11, XTUPLE_0:1;
hence x in n9 ; :: thesis: verum

end;

now :: thesis: for x being object st x in n9 holds
x in dom b

let x be object ; :: thesis: ( x in n9 implies x in dom b )
assume x in n9 ; :: thesis: x in dom b
then reconsider k = x as Element of n9 ;
[k,((b2 . k) -' (b1 . k))] in b ;
hence x in dom b by XTUPLE_0:def 12; :: thesis: verum

end;

then A12: dom b = n9 by A9, TARSKI:2;
then reconsider b = b as ManySortedSet of n9 by PARTFUN1:def 2, RELAT_1:def 18;

A13: now :: thesis: for k being set st k in n holds
b . k = (b2 . k) -' (b1 . k)

let k be set ; :: thesis: ( k in n implies b . k = (b2 . k) -' (b1 . k) )
assume k in n ; :: thesis: b . k = (b2 . k) -' (b1 . k)
then consider u being object such that
A14: [k,u] in b by A12, XTUPLE_0:def 12;
consider k9 being Element of n9 such that
A15: [k,u] = [k9,((b2 . k9) -' (b1 . k9))] by A14;
A16: u = (b2 . k9) -' (b1 . k9) by A15, XTUPLE_0:1;
k = k9 by A15, XTUPLE_0:1;
hence b . k = (b2 . k) -' (b1 . k) by A14, A16, FUNCT_1:1; :: thesis: verum

end;

now :: thesis: for x being object st x in support b holds
x in support b2

let x be object ; :: thesis: ( x in support b implies x in support b2 )
A17: support b c= dom b by PRE_POLY:37;
assume A18: x in support b ; :: thesis: x in support b2
then A19: b . x <> 0 by PRE_POLY:def 7;

now :: thesis: x in support b2

assume not x in support b2 ; :: thesis: contradiction
then b2 . x = 0 by PRE_POLY:def 7;
then 0 = (b2 . x) -' (b1 . x) by NAT_2:8;
hence contradiction by A12, A13, A18, A19, A17; :: thesis: verum

end;

hence x in support b2 ; :: thesis: verum

end;

then A20: support b c= support b2 ;

now :: thesis: for x being object st x in rng b holds
x in NAT

let x be object ; :: thesis: ( x in rng b implies x in NAT )
assume x in rng b ; :: thesis: x in NAT
then consider y being object such that
A21: [y,x] in b by XTUPLE_0:def 13;
consider k being Element of n9 such that
A22: [y,x] = [k,((b2 . k) -' (b1 . k))] by A21;
x = (b2 . k) -' (b1 . k) by A22, XTUPLE_0:1;
hence x in NAT ; :: thesis: verum

end;

then rng b c= NAT ;
then reconsider b = b as bag of n by A20, PRE_POLY:def 8, VALUED_0:def 6;
take b = b; :: thesis: ex b being bag of n st b2 = b1 + b

now :: thesis: for k being object st k in n holds
(b1 . k) + (b . k) = b2 . k

let k be object ; :: thesis: ( k in n implies (b1 . k) + (b . k) = b2 . k )
A23: 0 <= (b2 . k) - (b1 . k) by A2;
assume k in n ; :: thesis: (b1 . k) + (b . k) = b2 . k
hence (b1 . k) + (b . k) = (b1 . k) + ((b2 . k) -' (b1 . k)) by A13
.= (b1 . k) + ((b2 . k) + (- (b1 . k))) by A23, XREAL_0:def 2
.= b2 . k ;
:: thesis: verum

end;

then b2 = b1 + b by PRE_POLY:33;
hence ex b being bag of n st b2 = b1 + b ; :: thesis: verum

end;

end;

end;

hence ex b being bag of n st b2 = b1 + b ; :: thesis: verum

end;

hence ( b1 divides b2 iff ex b being bag of n st b2 = b1 + b ) by PRE_POLY:50; :: thesis: verum