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

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

A2: now

let k be set ; :: 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:11;
hence 0 <= (b2 . k) - (b1 . k) ; :: thesis: verum

end;

now

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

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

end;

now

let x, y1, y2 be set ; :: 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,y1] `1 by A7, MCART_1:def 1
.= x by MCART_1:def 1
.= [x,y2] `1 by MCART_1:def 1
.= k9 by A8, MCART_1:def 1 ;
hence y1 = [x,y2] `2 by A7, A8, MCART_1:def 2
.= y2 by MCART_1:def 2 ;
:: 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

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

end;

now

let x be set ; :: 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 RELAT_1:def 4; :: thesis: verum

end;

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

A13: now

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 set such that
A14: [k,u] in b by A12, RELAT_1:def 4;
consider k9 being Element of n9 such that
A15: [k,u] = [k9,((b2 . k9) -' (b1 . k9))] by A14;
A16: u = [k9,((b2 . k9) -' (b1 . k9))] `2 by A15, MCART_1:def 2
.= (b2 . k9) -' (b1 . k9) by MCART_1:def 2 ;
k = [k9,((b2 . k9) -' (b1 . k9))] `1 by A15, MCART_1:def 1
.= k9 by MCART_1:def 1 ;
hence b . k = (b2 . k) -' (b1 . k) by A14, A16, FUNCT_1:8; :: thesis: verum

end;

now

let x be set ; :: 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

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:10;
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 by TARSKI:def 3;

now

let x be set ; :: thesis: ( x in rng b implies x in NAT )
assume x in rng b ; :: thesis: x in NAT
then consider y being set such that
A21: [y,x] in b by RELAT_1:def 5;
consider k being Element of n9 such that
A22: [y,x] = [k,((b2 . k) -' (b1 . k))] by A21;
x = [k,((b2 . k) -' (b1 . k))] `2 by A22, MCART_1:def 2
.= (b2 . k) -' (b1 . k) by MCART_1:def 2 ;
hence x in NAT ; :: thesis: verum

end;

then rng b c= NAT by TARSKI:def 3;
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

let k be set ; :: 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