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

now

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

A2: now

let k be set ; :: thesis: 0 <= (b2 . k) - (b1 . k)
b1 . k <= b2 . k by A1, POLYNOM1:def 13;
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 st b2 = b1 + b

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

end;

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

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

A4: now

let x be set ; :: thesis: ( x in { [k,((b2 . k) -' (b1 . k))] where k is Element of n' : verum } implies ex y, z being set st x = [y,z] )
assume x in { [k,((b2 . k) -' (b1 . k))] where k is Element of n' : verum } ; :: thesis: ex y, z being set st x = [y,z]
then consider k being Element of n' such that
A5: x = [k,((b2 . k) -' (b1 . k))] ;
thus ex y, z being set st x = [y,z] by A5; :: thesis: verum

end;

now

let x, y1, y2 be set ; :: thesis: ( [x,y1] in { [k,((b2 . k) -' (b1 . k))] where k is Element of n' : verum } & [x,y2] in { [k,((b2 . k) -' (b1 . k))] where k is Element of n' : verum } implies y1 = y2 )
assume A6: ( [x,y1] in { [k,((b2 . k) -' (b1 . k))] where k is Element of n' : verum } & [x,y2] in { [k,((b2 . k) -' (b1 . k))] where k is Element of n' : verum } ) ; :: thesis: y1 = y2
then consider k being Element of n' such that
A7: [x,y1] = [k,((b2 . k) -' (b1 . k))] ;
consider k' being Element of n' such that
A8: [x,y2] = [k',((b2 . k') -' (b1 . k'))] 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
.= k' 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 n' : 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 n' )
assume x in dom b ; :: thesis: x in n'
then consider y being set such that
A10: [x,y] in b by RELAT_1:def 4;
consider k being Element of n' 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 n' ; :: thesis: verum

end;

now

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

end;

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

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
A13: [y,x] in b by RELAT_1:def 5;
consider k being Element of n' such that
A14: [y,x] = [k,((b2 . k) -' (b1 . k))] by A13;
x = [k,((b2 . k) -' (b1 . k))] `2 by A14, MCART_1:def 2
.= (b2 . k) -' (b1 . k) by MCART_1:def 2 ;
hence x in NAT ; :: thesis: verum

end;

then A15: rng b c= NAT by TARSKI:def 3;

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

end;

now

let x be set ; :: thesis: ( x in support b implies x in support b2 )
assume A20: x in support b ; :: thesis: x in support b2
then A21: b . x <> 0 by POLYNOM1:def 7;
A22: support b c= dom b by POLYNOM1:41;

now

assume not x in support b2 ; :: thesis: contradiction
then b2 . x = 0 by POLYNOM1:def 7;
then 0 = (b2 . x) -' (b1 . x) by NAT_2:10;
hence contradiction by A12, A16, A20, A21, A22; :: thesis: verum

end;

hence x in support b2 ; :: thesis: verum

end;

then support b c= support b2 by TARSKI:def 3;
then support b is finite ;
then reconsider b = b as bag of by A15, POLYNOM1:def 8, VALUED_0:def 6;
take b = b; :: thesis: ex b being bag of st b2 = b1 + b

now

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

end;

then b2 = b1 + b by POLYNOM1:37;
hence ex b being bag of st b2 = b1 + b ; :: thesis: verum

end;

end;

end;

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

end;

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