bagord_2.miz

begin

 theorem :: BAGORD_2:1



 Th6: for m,n be Nat holds n = ((m -' (m -' n)) + (n -' m))

 proof

 let m,n be Nat;

 per cases ;

 suppose m <= n;

 then

 A1: (m -' n) = 0 & (n -' m) = (n - m) by NAT_2: 8, XREAL_1: 233;

 then (m -' (m -' n)) = m by NAT_D: 40;

 hence thesis by A1;

 end;

 suppose m > n;

 then (n -' m) = 0 & (m -' (m -' n)) = n & (n + 0 ) = n by NAT_D: 58, NAT_2: 8;

 hence thesis;

 end;

 end;

 theorem :: BAGORD_2:2

 for n,m be Nat holds (m -' n) >= (m - n) by XREAL_0:def 2;

 theorem :: BAGORD_2:3



 Th5: for m,n,x,y be Nat st n = ((m -' x) + y) holds (m -' n) <= x & (n -' m) <= y

 proof

 let m,n,x,y be Nat such that

 A0: n = ((m -' x) + y);

 per cases ;

 suppose m <= n;

 then

 A1: (m -' n) = 0 & (n -' m) = (n - m) by NAT_2: 8, XREAL_1: 233;

 n <= (m + y) by A0, XREAL_1: 6, NAT_D: 35;

 hence thesis by A1, XREAL_1: 20;

 end;

 suppose m > n;

 then

 A2: (n -' m) = 0 & (m -' (m -' n)) = n >= (m -' x) by A0, NAT_D: 58, NAT_1: 11, NAT_2: 8;

 (m -' (m -' n)) = (m - (m -' n)) & (m -' x) >= (m - x) by XREAL_0:def 2, XREAL_1: 233, NAT_D: 35;

 then (m - (m -' n)) >= (m - x) by A2, XXREAL_0: 2;

 hence thesis by XREAL_1: 10, A2;

 end;

 end;

 theorem :: BAGORD_2:4



 Th5A: for m,n,x,y be Nat st x <= m & n = ((m -' x) + y) holds (x -' (m -' n)) = (y -' (n -' m))

 proof

 let m,n,x,y be Nat;

 assume

 Z0: x <= m;

 assume

 Z1: n = ((m -' x) + y);

 then (m -' n) <= x & (n -' m) <= y by Th5;

 then

 A2: (x -' (m -' n)) = (x - (m -' n)) & (y -' (n -' m)) = (y - (n -' m)) by XREAL_1: 233;



 A3: (n - y) = (m - x) by Z0, Z1, XREAL_1: 233;

 per cases ;

 suppose m <= n;

 then

 A4: (m -' n) = 0 & (n -' m) = (n - m) by NAT_2: 8, XREAL_1: 233;



 hence (x -' (m -' n)) = x by A2

 .= ((y - n) + m) by A3

 .= (y -' (n -' m)) by A2, A4;

 end;

 suppose m > n;

 then

 A5: (n -' m) = 0 & (m -' n) = (m - n) by NAT_2: 8, XREAL_1: 233;



 hence (x -' (m -' n)) = ((x - m) + n) by A2

 .= y by A3

 .= (y -' (n -' m)) by A2, A5;

 end;

 end;

 theorem :: BAGORD_2:5



 Th14: for k,x1,x2,y1,y2 be Nat st x2 <= k & x1 <= ((k -' x2) + y2) holds (x2 + (x1 -' y2)) <= k & ((((k -' x2) + y2) -' x1) + y1) = ((k -' (x2 + (x1 -' y2))) + ((y2 -' x1) + y1))

 proof

 let k,x1,x2,y1,y2 be Nat;

 assume

 Z0: x2 <= k;

 then

 A1: (k -' x2) = (k - x2) by XREAL_1: 233;

 assume

 Z1: x1 <= ((k -' x2) + y2);

 thus (x2 + (x1 -' y2)) <= k

 proof

 per cases ;

 suppose x1 < y2;

 then (x1 -' y2) = 0 by NAT_2: 8;

 hence thesis by Z0;

 end;

 suppose x1 >= y2;

 then (x1 -' y2) = (x1 - y2) by XREAL_1: 233;

 then (x1 -' y2) <= (((k - x2) + y2) - y2) = (k - x2) by A1, Z1, XREAL_1: 9;

 then (x2 + (x1 -' y2)) <= ((k - x2) + x2) by XREAL_1: 6;

 hence thesis;

 end;

 end;

 then

 A2: (k -' (x2 + (x1 -' y2))) = (k - (x2 + (x1 -' y2))) & (((k -' x2) + y2) -' x1) = (((k - x2) + y2) - x1) by Z1, A1, XREAL_1: 233;

 per cases ;

 suppose x1 <= y2;

 then (x1 -' y2) = 0 & (y2 -' x1) = (y2 - x1) by XREAL_1: 233, NAT_2: 8;

 hence ((((k -' x2) + y2) -' x1) + y1) = ((k -' (x2 + (x1 -' y2))) + ((y2 -' x1) + y1)) by A2;

 end;

 suppose x1 > y2;

 then (y2 -' x1) = 0 & (x1 -' y2) = (x1 - y2) by XREAL_1: 233, NAT_2: 8;

 hence ((((k -' x2) + y2) -' x1) + y1) = ((k -' (x2 + (x1 -' y2))) + ((y2 -' x1) + y1)) by A2;

 end;

 end;

 ::$Canceled

 reserve a,b for object,

I,J for set;

 registration

 cluster asymmetric transitive non empty for RelStr;

 existence

 proof

 set X = { 0 };

 set r = ( {} [:X, X:]);

 take R = RelStr (# X, r #);

 thus R is asymmetric

 proof

 let a, b;

 assume a in the carrier of R & b in the carrier of R;

 thus thesis;

 end;

 thus R is transitive

 proof

 let a;

 thus thesis;

 end;

 thus thesis;

 end;

 end

 registration

 let I;

 cluster asymmetric transitive for Relation of I;

 existence

 proof

 set X = I;

 take r = ( {} [:X, X:]);

 thus r is asymmetric

 proof

 let a, b;

 thus thesis;

 end;

 thus r is transitive

 proof

 let a;

 thus thesis;

 end;

 end;

 end

 registration

 let R be asymmetric RelStr;

 cluster the InternalRel of R -> asymmetric;

 coherence by NECKLACE:def 4;

 end

 registration

 let I;

 let p,q be I -valued FinSequence;

 cluster (p ^ q) -> I -valued;

 coherence

 proof

 ( rng p) c= I & ( rng q) c= I by RELAT_1:def 19;

 then ( rng (p ^ q)) = (( rng p) \/ ( rng q)) c= I by FINSEQ_1: 31, XBOOLE_1: 8;

 hence ( rng (p ^ q)) c= I;

 end;

 end

 theorem :: BAGORD_2:7



 Lem8: for p,q be FinSequence st (p ^ q) is I -valued holds p is I -valued & q is I -valued

 proof

 let p,q be FinSequence;

 assume

 Z1: ( rng (p ^ q)) c= I;



 A1: ( rng (p ^ q)) = (( rng p) \/ ( rng q)) by FINSEQ_1: 31;

 ( rng p) c= (( rng p) \/ ( rng q)) by XBOOLE_1: 7;

 hence ( rng p) c= I by Z1, A1, XBOOLE_1: 1;

 ( rng q) c= (( rng p) \/ ( rng q)) by XBOOLE_1: 7;

 hence ( rng q) c= I by Z1, A1, XBOOLE_1: 1;

 end;

 registration

 let I;

 let f be I -valued FinSequence;

 let n be Nat;

 cluster (f | n) -> I -valued;

 coherence ;

 end

 theorem :: BAGORD_2:8



 Lem9: for p be FinSequence st a in ( rng p) holds ex q,r be FinSequence st p = ((q ^ <*a*>) ^ r)

 proof

 let p be FinSequence;

 assume a in ( rng p);

 then

 consider i be object such that

 A1: i in ( dom p) & a = (p . i) by FUNCT_1:def 3;

 reconsider i as Nat by A1;



 A3: 1 <= i <= ( len p) by A1, FINSEQ_3: 25;

 consider k be Nat such that

 A2: i = (1 + k) by NAT_1: 10, A1, FINSEQ_3: 25;

 set q = ((1,k) -cut p);

 set r = (((i + 1),( len p)) -cut p);

 take q, r;

 k <= i & ((i,i) -cut p) = <*a*> by A1, A3, A2, NAT_1: 11, FINSEQ_6: 132;

 hence p = ((q ^ <*a*>) ^ r) by A3, A2, FINSEQ_6: 136;

 end;

 theorem :: BAGORD_2:9



 Lem12: for p,q be FinSequence holds p c< q iff ( len p) < ( len q) & for i be Nat st i in ( dom p) holds (p . i) = (q . i)

 proof

 let p,q be FinSequence;

 hereby

 assume

 Z0: p c< q;

 hence ( len p) < ( len q) by TREES_1: 6;

 p c= q by Z0, XBOOLE_0:def 8;

 hence for i be Nat st i in ( dom p) holds (p . i) = (q . i) by FOMODEL0: 51;

 end;

 assume

 Z2: ( len p) < ( len q);

 then ( dom p) c< ( dom q) by FINSEQ_3: 118;

 then

 A1: ( dom p) c= ( dom q) by XBOOLE_0:def 8;

 assume for i be Nat st i in ( dom p) holds (p . i) = (q . i);

 then for i be set st i in ( dom p) holds i in ( dom q) & (p . i) = (q . i) by A1;

 hence p c< q by Z2, XBOOLE_0:def 8, FOMODEL0: 51;

 end;

 theorem :: BAGORD_2:10



 Lem13: for p,q,r be FinSequence holds (r ^ p) c< (r ^ q) iff p c< q

 proof

 let p,q,r be FinSequence;

 thus (r ^ p) c< (r ^ q) implies p c< q

 proof

 assume

 A0: (r ^ p) c< (r ^ q);

 ( len (r ^ p)) = (( len r) + ( len p)) & ( len (r ^ q)) = (( len r) + ( len q)) by FINSEQ_1: 22;

 then

 A2: ( len p) < ( len q) by A0, Lem12, XREAL_1: 6;

 then

 A3: ( dom p) c= ( dom q) by FINSEQ_3: 30;

 for i be Nat st i in ( dom p) holds (p . i) = (q . i)

 proof

 let i be Nat;

 assume i in ( dom p);

 then (p . i) = ((r ^ p) . (( len r) + i)) & (q . i) = ((r ^ q) . (( len r) + i)) & (( len r) + i) in ( dom (r ^ p)) by A3, FINSEQ_1:def 7, FINSEQ_1: 28;

 hence thesis by A0, Lem12;

 end;

 hence thesis by A2, Lem12;

 end;

 assume p c< q;

 then (r ^ p) c= (r ^ q) & (r ^ p) <> (r ^ q) by FINSEQ_6: 13, FINSEQ_1: 33, XBOOLE_0:def 8;

 hence thesis by XBOOLE_0:def 8;

 end;

 definition

 let R be asymmetric non empty RelStr;

 let x,y be Element of R;

 :: original: <=

 redefine

 pred x <= y;

 asymmetry

 proof

 let a,b be Element of R;

 assume [a, b] in the InternalRel of R;

 hence not [b, a] in the InternalRel of R by PREFER_1: 22;

 end;

 end

 theorem :: BAGORD_2:11



 Lem2: for R be asymmetric non empty RelStr holds for x,y be Element of R holds x <= y iff x < y

 proof

 let R be asymmetric non empty RelStr;

 let x,y be Element of R;

 hereby

 assume

 Z0: x <= y;

 then x <> y;

 hence x < y by Z0, ORDERS_2:def 6;

 end;

 assume x < y;

 hence x <= y by ORDERS_2:def 6;

 end;

 begin

 definition

 let I;

 mode multiset of I is Element of ( finite-MultiSet_over I);

 end

 registration

 let I;

 cluster -> I -defined natural-valued for multiset of I;

 coherence

 proof

 let m be multiset of I;

 m in the carrier of ( finite-MultiSet_over I) c= the carrier of ( MultiSet_over I) by MONOID_0: 23;

 hence thesis by MONOID_1: 27;

 end;

 end

 registration

 let I;

 cluster -> total for multiset of I;

 coherence

 proof

 let m be multiset of I;

 m in the carrier of ( finite-MultiSet_over I) c= the carrier of ( MultiSet_over I) by MONOID_0: 23;

 then m is Function of I, NAT by MONOID_1: 27;

 hence thesis;

 end;

 end

 definition

 let m be natural-valued Function;

 :: original: support

 redefine

 :: BAGORD_2:def1

 func support m equals (m " ( NAT \ { 0 }));

 compatibility

 proof

 let I;

 ( support m) = (m " ( NAT \ { 0 }))

 proof

 thus ( support m) c= (m " ( NAT \ { 0 }))

 proof

 let a;

 assume a in ( support m);

 then

 A1: (m . a) <> 0 by PRE_POLY:def 7;

 then

 A2: a in ( dom m) by FUNCT_1:def 2;

 (m . a) in NAT & not (m . a) in { 0 } by A1, TARSKI:def 1, ORDINAL1:def 12;

 then (m . a) in ( NAT \ { 0 }) by XBOOLE_0:def 5;

 hence thesis by A2, FUNCT_1:def 7;

 end;

 let a;

 assume a in (m " ( NAT \ { 0 }));

 then (m . a) in ( NAT \ { 0 }) by FUNCT_1:def 7;

 then not (m . a) in { 0 } by XBOOLE_0:def 5;

 then (m . a) <> 0 by TARSKI:def 1;

 hence thesis by PRE_POLY:def 7;

 end;

 hence I = ( support m) iff I = (m " ( NAT \ { 0 }));

 end;

 end

 registration

 let I;

 cluster -> finite-support for multiset of I;

 coherence

 proof

 let m be multiset of I;

 m in the carrier of ( finite-MultiSet_over I) c= the carrier of ( MultiSet_over I) by MONOID_0: 23;

 then ( support m) is finite by MONOID_1:def 6;

 hence thesis by PRE_POLY:def 8;

 end;

 end

 theorem :: BAGORD_2:12



 Th1: a is multiset of I iff a is bag of I

 proof

 thus a is multiset of I implies a is bag of I;

 assume a is bag of I;

 then

 reconsider b = a as bag of I;

 ( dom b) = I & ( rng b) c= NAT by PARTFUN1:def 2, VALUED_0:def 6;

 then b is Function of I, NAT by FUNCT_2: 2;

 then b is Multiset of I & ( support b) is finite by MONOID_1: 27;

 hence thesis by MONOID_1:def 6;

 end;

 theorem :: BAGORD_2:13



 Th11: ( 1. ( finite-MultiSet_over I)) = ( EmptyBag I)

 proof

 ( 1. ( MultiSet_over I)) = (I --> 0 ) = ( EmptyBag I) by MONOID_1: 26;

 hence thesis by MONOID_0:def 24;

 end;

 definition

 let R be RelStr;

 let x,y be Element of R;

 :: BAGORD_2:def2

 pred x ## y means not x <= y & not y <= x;

 symmetry ;

 end

 definition

 struct ( multMagma, RelStr) RelMultMagma (# the carrier -> set,

the multF -> BinOp of the carrier,

the InternalRel -> Relation of the carrier #)

 attr strict strict;

 end

 definition

 struct ( multLoopStr, RelStr) RelMonoid (# the carrier -> set,

the multF -> BinOp of the carrier,

the OneF -> Element of the carrier,

the InternalRel -> Relation of the carrier #)

 attr strict strict;

 end

 definition

 let M be multLoopStr;

 :: BAGORD_2:def3

 mode RelExtension of M -> RelMonoid means

 : RE: the multLoopStr of it = the multLoopStr of M;

 existence

 proof

 set r = the Relation of the carrier of M;

 take R = RelMonoid (# the carrier of M, the multF of M, the OneF of M, r #);

 thus thesis;

 end;

 end

 registration

 let M be non empty multLoopStr;

 cluster -> non empty for RelExtension of M;

 coherence

 proof

 let R be RelExtension of M;

 the multLoopStr of R = the multLoopStr of M by RE;

 hence thesis;

 end;

 end

 registration

 let M be multLoopStr;

 cluster strict for RelExtension of M;

 existence

 proof

 set r = the Relation of the carrier of M;

 set R = RelMonoid (# the carrier of M, the multF of M, the OneF of M, r #);

 the multLoopStr of R = the multLoopStr of M;

 then R is RelExtension of M by RE;

 hence thesis;

 end;

 end

 theorem :: BAGORD_2:14



 Th2: for N be multLoopStr, M be RelExtension of N holds a is Element of M iff a is Element of N

 proof

 let N be multLoopStr;

 let M be RelExtension of N;

 the multLoopStr of N = the multLoopStr of M by RE;

 hence thesis;

 end;

 theorem :: BAGORD_2:15



 Th3: for N be multLoopStr, M be RelExtension of N holds ( 1. N) = ( 1. M)

 proof

 let N be multLoopStr;

 let M be RelExtension of N;

 the multLoopStr of N = the multLoopStr of M by RE;

 hence thesis;

 end;

 registration

 let I;

 let M be RelExtension of ( finite-MultiSet_over I);

 cluster -> Function-like Relation-like for Element of M;

 coherence

 proof

 let m be Element of M;

 m is multiset of I by Th2;

 hence thesis;

 end;

 end

 registration

 let I;

 let M be RelExtension of ( finite-MultiSet_over I);

 cluster -> I -defined natural-valued finite-support for Element of M;

 coherence

 proof

 let m be Element of M;

 m is multiset of I by Th2;

 hence thesis;

 end;

 end

 registration

 let I;

 let M be RelExtension of ( finite-MultiSet_over I);

 cluster -> total for Element of M;

 coherence

 proof

 let m be Element of M;

 m is multiset of I by Th2;

 hence thesis;

 end;

 end

 theorem :: BAGORD_2:16

 for M be RelExtension of ( finite-MultiSet_over I) holds the carrier of M = ( Bags I)

 proof

 set N = ( finite-MultiSet_over I);

 let M be RelExtension of ( finite-MultiSet_over I);

 thus the carrier of M c= ( Bags I)

 proof

 let a;

 assume a in the carrier of M;

 hence a in ( Bags I) by PRE_POLY:def 12;

 end;

 let a;

 assume a in ( Bags I);

 then a is bag of I by PRE_POLY:def 12;

 then a is Element of N by Th1;

 then a is Element of M by Th2;

 hence thesis;

 end;

 scheme :: BAGORD_2:sch1

 RelEx { M() -> non empty multLoopStr , R[ object, object] } :

ex N be strict RelExtension of M() st for x,y be Element of N holds x <= y iff R[x, y];

 consider R be Relation of the carrier of M() such that

 A1: for x,y be Element of M() holds [x, y] in R iff R[x, y] from RELSET_1:sch 2;

 set N = RelMonoid (# the carrier of M(), the multF of M(), the OneF of M(), R #);

 the multLoopStr of N = the multLoopStr of M();

 then

 reconsider N as strict RelExtension of M() by RE;

 take N;

 let x,y be Element of N;

 [x, y] in R iff R[x, y] by A1;

 hence thesis by ORDERS_2:def 5;

 end;

 theorem :: BAGORD_2:17



 Th4: for N be multLoopStr, M1,M2 be strict RelExtension of N st for m,n be Element of M1 holds for x,y be Element of M2 st m = x & n = y holds m <= n iff x <= y holds M1 = M2

 proof

 let N be multLoopStr;

 let M1,M2 be strict RelExtension of N;

 assume

 Z4: for m,n be Element of M1 holds for x,y be Element of M2 st m = x & n = y holds m <= n iff x <= y;



 A2: the multLoopStr of M1 = the multLoopStr of N & the multLoopStr of M2 = the multLoopStr of N by RE;

 the InternalRel of M1 = the InternalRel of M2

 proof

 let a, b;

 hereby

 assume

 A3: [a, b] in the InternalRel of M1;

 then

 reconsider m = a, n = b as Element of M1 by ZFMISC_1: 87;

 reconsider x = m, y = n as Element of M2 by A2;

 m <= n by A3, ORDERS_2:def 5;

 then x <= y by Z4;

 hence [a, b] in the InternalRel of M2 by ORDERS_2:def 5;

 end;

 assume

 A3: [a, b] in the InternalRel of M2;

 then

 reconsider m = a, n = b as Element of M2 by ZFMISC_1: 87;

 reconsider x = m, y = n as Element of M1 by A2;

 m <= n by A3, ORDERS_2:def 5;

 then x <= y by Z4;

 hence [a, b] in the InternalRel of M1 by ORDERS_2:def 5;

 end;

 hence M1 = M2 by A2;

 end;

 begin

 definition

 let R be non empty RelStr;

 :: BAGORD_2:def4

 func DershowitzMannaOrder R -> strict RelExtension of ( finite-MultiSet_over the carrier of R) means

 : DM: for m,n be Element of it holds m <= n iff ex x,y be Element of it st ( 1. it ) <> x divides n & m = ((n -' x) + y) & for b be Element of R st (y . b) > 0 holds ex a be Element of R st (x . a) > 0 & b <= a;

 existence

 proof

 set M = ( finite-MultiSet_over the carrier of R);

 defpred R[ bag of the carrier of R, bag of the carrier of R] means ex x,y be Element of M st ( 1. M) <> x divides $2 & $1 = (($2 -' x) + y) & for b be Element of R st (y . b) > 0 holds ex a be Element of R st (x . a) > 0 & b <= a;

 consider N be strict RelExtension of M such that

 A1: for m,n be Element of N holds m <= n iff R[m, n] from RelEx;

 take N;

 let m,n be Element of N;

 hereby

 assume m <= n;

 then

 consider x,y be Element of M such that

 A2: ( 1. M) <> x divides n & m = ((n -' x) + y) & for b be Element of R st (y . b) > 0 holds ex a be Element of R st (x . a) > 0 & b <= a by A1;

 reconsider x, y as Element of N by Th2;

 take x, y;

 thus ( 1. N) <> x divides n & m = ((n -' x) + y) & for b be Element of R st (y . b) > 0 holds ex a be Element of R st (x . a) > 0 & b <= a by A2, Th3;

 end;

 given x,y be Element of N such that

 A3: ( 1. N) <> x divides n & m = ((n -' x) + y) & for b be Element of R st (y . b) > 0 holds ex a be Element of R st (x . a) > 0 & b <= a;

 reconsider x, y as Element of M by Th2;

 ( 1. M) <> x divides n & m = ((n -' x) + y) & for b be Element of R st (y . b) > 0 holds ex a be Element of R st (x . a) > 0 & b <= a by A3, Th3;

 hence thesis by A1;

 end;

 uniqueness

 proof

 set M = ( finite-MultiSet_over the carrier of R);

 let N1,N2 be strict RelExtension of ( finite-MultiSet_over the carrier of R);

 assume that

 A1: for m,n be Element of N1 holds m <= n iff ex x,y be Element of N1 st ( 1. N1) <> x divides n & m = ((n -' x) + y) & for b be Element of R st (y . b) > 0 holds ex a be Element of R st (x . a) > 0 & b <= a and

 A2: for m,n be Element of N2 holds m <= n iff ex x,y be Element of N2 st ( 1. N2) <> x divides n & m = ((n -' x) + y) & for b be Element of R st (y . b) > 0 holds ex a be Element of R st (x . a) > 0 & b <= a;

 for m,n be Element of N1 holds for x,y be Element of N2 st m = x & n = y holds m <= n iff x <= y

 proof

 let m,n be Element of N1;

 let k,l be Element of N2;

 assume

 Z0: m = k;

 assume

 Z1: n = l;



 A5: ( 1. N1) = ( 1. M) = ( 1. N2) by Th3;

 hereby

 assume m <= n;

 then

 consider x,y be Element of N1 such that

 A3: ( 1. N1) <> x divides n & m = ((n -' x) + y) & for b be Element of R st (y . b) > 0 holds ex a be Element of R st (x . a) > 0 & b <= a by A1;

 reconsider x, y as Element of M by Th2;

 reconsider x, y as Element of N2 by Th2;

 ( 1. N2) <> x divides l & k = ((l -' x) + y) & for b be Element of R st (y . b) > 0 holds ex a be Element of R st (x . a) > 0 & b <= a by Z0, Z1, A3, A5;

 hence k <= l by A2;

 end;

 assume k <= l;

 then

 consider x,y be Element of N2 such that

 A4: ( 1. N2) <> x divides l & k = ((l -' x) + y) & for b be Element of R st (y . b) > 0 holds ex a be Element of R st (x . a) > 0 & b <= a by A2;

 reconsider x, y as Element of M by Th2;

 reconsider x, y as Element of N1 by Th2;

 ( 1. N1) <> x divides n & m = ((n -' x) + y) & for b be Element of R st (y . b) > 0 holds ex a be Element of R st (x . a) > 0 & b <= a by Z0, Z1, A4, A5;

 hence m <= n by A1;

 end;

 hence thesis by Th4;

 end;

 end

 theorem :: BAGORD_2:18



 Th7: for m,n be bag of I holds n = ((m -' (m -' n)) + (n -' m))

 proof

 let m,n be bag of I;

 let a;

 assume a in I;



 thus (n . a) = (((m . a) -' ((m . a) -' (n . a))) + ((n . a) -' (m . a))) by Th6

 .= (((m . a) -' ((m -' n) . a)) + ((n . a) -' (m . a))) by PRE_POLY:def 6

 .= (((m -' (m -' n)) . a) + ((n . a) -' (m . a))) by PRE_POLY:def 6

 .= (((m -' (m -' n)) . a) + ((n -' m) . a)) by PRE_POLY:def 6

 .= (((m -' (m -' n)) + (n -' m)) . a) by PRE_POLY:def 5;

 end;

 theorem :: BAGORD_2:19



 Th8: for m,n,x,y be bag of I st n = ((m -' x) + y) holds (m -' n) divides x & (n -' m) divides y

 proof

 let m,n,x,y be bag of I;

 assume

 Z0: n = ((m -' x) + y);

 thus (m -' n) divides x

 proof

 let a;

 (n . a) = (((m -' x) . a) + (y . a)) by Z0, PRE_POLY:def 5

 .= (((m . a) -' (x . a)) + (y . a)) by PRE_POLY:def 6;

 then ((m . a) -' (n . a)) <= (x . a) by Th5;

 hence ((m -' n) . a) <= (x . a) by PRE_POLY:def 6;

 end;

 let a;

 (n . a) = (((m -' x) . a) + (y . a)) by Z0, PRE_POLY:def 5

 .= (((m . a) -' (x . a)) + (y . a)) by PRE_POLY:def 6;

 then ((n . a) -' (m . a)) <= (y . a) by Th5;

 hence thesis by PRE_POLY:def 6;

 end;

 theorem :: BAGORD_2:20



 Th8A: for m,n,x,y be bag of I st x divides m & n = ((m -' x) + y) holds (x -' (m -' n)) = (y -' (n -' m))

 proof

 let m,n,x,y be bag of I;

 assume

 Z0: x divides m;

 assume

 Z1: n = ((m -' x) + y);

 let a;

 assume a in I;



 A1: (n . a) = (((m -' x) . a) + (y . a)) = (((m . a) -' (x . a)) + (y . a)) & (x . a) <= (m . a) by Z0, Z1, PRE_POLY:def 5, PRE_POLY:def 6, PRE_POLY:def 11;



 thus ((x -' (m -' n)) . a) = ((x . a) -' ((m -' n) . a)) by PRE_POLY:def 6

 .= ((x . a) -' ((m . a) -' (n . a))) by PRE_POLY:def 6

 .= ((y . a) -' ((n . a) -' (m . a))) by A1, Th5A

 .= ((y . a) -' ((n -' m) . a)) by PRE_POLY:def 6

 .= ((y -' (n -' m)) . a) by PRE_POLY:def 6;

 end;

 theorem :: BAGORD_2:21



 Th9: for m,x,y be bag of I st x divides m & x <> y holds m <> ((m -' x) + y)

 proof

 let m,x,y be bag of I;

 assume

 Z0: for a holds (x . a) <= (m . a);

 given a such that

 Z1: a in I & (x . a) <> (y . a);

 take a;

 thus a in I by Z1;



 A1: (((m -' x) + y) . a) = (((m -' x) . a) + (y . a)) = (((m . a) -' (x . a)) + (y . a)) by PRE_POLY:def 5, PRE_POLY:def 6;

 ((m . a) -' (x . a)) = ((m . a) - (x . a)) by Z0, XREAL_1: 233;

 hence thesis by A1, Z1;

 end;

 theorem :: BAGORD_2:22



 Lem5: for I be non empty set, R be Relation of I holds for r be RedSequence of R st ( len r) > 1 holds (r . ( len r)) in I

 proof

 let I be non empty set;

 let R be Relation of I;

 let r be RedSequence of R;

 assume

 Z0: ( len r) > 1;

 then

 consider i be Nat such that

 A1: ( len r) = (1 + i) by NAT_1: 10;

 ( len r) >= i >= 1 by Z0, A1, NAT_1: 13;

 then i in ( dom r) & (i + 1) in ( dom r) by A1, FINSEQ_3: 25, FINSEQ_5: 6;

 then [(r . i), (r . ( len r))] in R by A1, REWRITE1:def 2;

 hence (r . ( len r)) in I by ZFMISC_1: 87;

 end;

 theorem :: BAGORD_2:23



 Th13: for R be asymmetric transitive Relation of I holds for r be RedSequence of R holds r is one-to-one

 proof

 let R be asymmetric transitive Relation of I;

 let r be RedSequence of R;

 let a, b;

 assume

 Z0: a in ( dom r) & b in ( dom r);

 then

 reconsider i = a, j = b as Nat;

 assume

 Z1: (r . a) = (r . b) & a <> b;



 A1: for i,j be Nat st i > j & i in ( dom r) & j in ( dom r) holds (r . i) <> (r . j)

 proof

 let i,j be Nat;

 assume i > j;

 then

 A1: i >= (j + 1) by NAT_1: 13;

 assume

 Z3: i in ( dom r);

 assume

 Z4: j in ( dom r);

 defpred P[ Nat] means $1 in ( dom r) implies [(r . j), (r . $1)] in R & (r . $1) <> (r . j);



 A2: P[(j + 1)]

 proof

 assume (j + 1) in ( dom r);

 hence [(r . j), (r . (j + 1))] in R by Z4, REWRITE1:def 2;

 hence thesis by PREFER_1: 22;

 end;



 A3: for i be Nat st i >= (j + 1) & P[i] holds P[(i + 1)]

 proof

 let i be Nat;

 assume

 Z5: i >= (j + 1) & P[i] & (i + 1) in ( dom r);

 then 1 <= (j + 1) & i < (i + 1) <= ( len r) by NAT_1: 11, NAT_1: 13, FINSEQ_3: 25;

 then 1 <= i <= ( len r) by Z5, XXREAL_0: 2;

 then i in ( dom r) by FINSEQ_3: 25;

 then

 ZZ: [(r . j), (r . i)] in R & [(r . i), (r . (i + 1))] in R by Z5, REWRITE1:def 2;

 hence [(r . j), (r . (i + 1))] in R by RELAT_2: 31;

 thus thesis by PREFER_1: 22, RELAT_2: 31, ZZ;

 end;

 for i be Nat st i >= (j + 1) holds P[i] from NAT_1:sch 8( A2, A3);

 hence (r . i) <> (r . j) by A1, Z3;

 end;

 i < j or j < i by Z1, XXREAL_0: 1;

 hence thesis by Z0, Z1, A1;

 end;

 theorem :: BAGORD_2:24



 Th12: for R be asymmetric transitive non empty RelStr holds for X be set st X is finite & ex x be Element of R st x in X holds ex x be Element of R st x is_maximal_in X

 proof

 let R be asymmetric transitive non empty RelStr;

 let X be set;

 assume X is finite;

 then

 reconsider X1 = X as finite set;

 given x be Element of R such that

 Z1: x in X;

 set Y = { r where r be Element of (X1 * ) : r is RedSequence of the InternalRel of R };

 defpred P[ Nat] means ex r be RedSequence of the InternalRel of R st r in Y & ( len r) = $1;



 A1: for k be Nat st P[k] holds k <= ( card X1)

 proof

 let k be Nat;

 given r be RedSequence of the InternalRel of R such that

 A2: r in Y & ( len r) = k;

 consider q be Element of (X1 * ) such that

 A3: r = q & q is RedSequence of the InternalRel of R by A2;

 ( rng r) c= X1 & r is one-to-one by A3, Th13, FINSEQ_1:def 4;

 then ( len r) = ( card ( rng r)) <= ( card X1) by PRE_POLY: 19, NAT_1: 43;

 hence thesis by A2;

 end;



 B1: P[1]

 proof

 set k = 1;

 reconsider r = <*x*> as RedSequence of the InternalRel of R by REWRITE1: 6;

 take r;

 <*x*> is FinSequence of X1 by Z1, FINSEQ_1: 74;

 then <*x*> in (X1 * ) by FINSEQ_1:def 11;

 hence r in Y;

 thus ( len r) = k by FINSEQ_1: 39;

 end;

 then

 A4: ex k be Nat st P[k];

 consider k be Nat such that

 A5: P[k] & for n be Nat st P[n] holds n <= k from NAT_1:sch 6( A1, A4);

 consider r be RedSequence of the InternalRel of R such that

 A6: r in Y & ( len r) = k by A5;

 consider q be Element of (X1 * ) such that

 A7: r = q & q is RedSequence of the InternalRel of R by A6;

 1 <= k by B1, A5;

 per cases by XXREAL_0: 1;

 suppose

 C1: k = 1;

 take x;

 not ex y be Element of R st y in X & x < y

 proof

 given y be Element of R such that

 A8: y in X & x < y;

 [x, y] in the InternalRel of R by A8, ORDERS_2:def 5, ORDERS_2:def 6;

 then

 reconsider r = <*x, y*> as RedSequence of the InternalRel of R by REWRITE1: 7;

 <*x, y*> is FinSequence of X1 by Z1, A8, FINSEQ_2: 13;

 then r in (X1 * ) by FINSEQ_1:def 11;

 then r in Y & ( len r) = 2 by FINSEQ_1: 44;

 hence contradiction by A5, C1;

 end;

 hence x is_maximal_in X by Z1, WAYBEL_4: 55;

 end;

 suppose

 A8: k > 1;

 then

 reconsider x = (r . k) as Element of R by A6, Lem5;

 take x;



 A9: k in ( dom r) & r is FinSequence of X1 by A6, A7, FINSEQ_5: 6;

 not ex y be Element of R st y in X & x < y

 proof

 given y be Element of R such that

 B1: y in X & x < y;

 [x, y] in the InternalRel of R by B1, ORDERS_2:def 5, ORDERS_2:def 6;

 then

 reconsider p = <*x, y*> as RedSequence of the InternalRel of R by REWRITE1: 7;

 (p . 1) = x by FINSEQ_1: 44;

 then

 reconsider rp = (r $^ p) as RedSequence of the InternalRel of R by A6, REWRITE1: 8;

 ex i be Nat st k = (1 + i) by A8, NAT_1: 10;

 then

 consider t be FinSequence, a such that

 B2: r = (t ^ <*a*>) by A6, FINSEQ_2: 18;

 k = (( len t) + 1) by A6, B2, FINSEQ_2: 16;

 then x = a by B2, FINSEQ_1: 42;

 then

 B3: rp = (r ^ <*y*>) by B2, REWRITE1: 3;

 reconsider yy = <*y*>, r1 = r as FinSequence of X1 by A7, B1, FINSEQ_1: 74;

 (r1 ^ yy) is FinSequence of X1;

 then rp in (X1 * ) by B3, FINSEQ_1:def 11;

 then rp in Y & ( len rp) = (k + 1) by A6, B3, FINSEQ_2: 16;

 then (k + 1) <= k by A5;

 hence contradiction by NAT_1: 13;

 end;

 hence x is_maximal_in X by A9, FUNCT_1: 102, WAYBEL_4: 55;

 end;

 end;

 theorem :: BAGORD_2:25



 Lem3: for m,n be bag of I holds (m -' n) divides m

 proof

 let m,n be bag of I;

 let a;

 ((m . a) -' (n . a)) <= (m . a) by NAT_D: 35;

 hence ((m -' n) . a) <= (m . a) by PRE_POLY:def 6;

 end;

 registration

 let I;

 cluster -> Function-like Relation-like for Element of ( Bags I);

 coherence by PRE_POLY:def 12;

 end

 theorem :: BAGORD_2:26



 Lem4: for m,n be bag of I holds (m -' n) <> ( EmptyBag I) or m = n or (n -' m) <> ( EmptyBag I)

 proof

 let m,n be bag of I;

 assume

 Z0: (m -' n) = ( EmptyBag I);

 assume m <> n;

 then

 consider a such that

 A1: a in I & (m . a) <> (n . a) by PBOOLE:def 10;

 per cases by A1, XXREAL_0: 1;

 suppose (m . a) > (n . a);

 then ((m . a) - (n . a)) > 0 by XREAL_1: 50;

 then ((m . a) -' (n . a)) > 0 by XREAL_0:def 2;

 then 0 < ((m -' n) . a) = 0 by A1, Z0, FUNCOP_1: 7, PRE_POLY:def 6;

 hence thesis;

 end;

 suppose

 A3: (n . a) > (m . a);

 take a;

 thus a in I by A1;

 ((n . a) - (m . a)) > 0 by A3, XREAL_1: 50;

 then ((n . a) -' (m . a)) > 0 by XREAL_0:def 2;

 then ((n -' m) . a) > 0 by PRE_POLY:def 6;

 hence ((n -' m) . a) <> (( EmptyBag I) . a) by A1, FUNCOP_1: 7;

 end;

 end;

 definition

 let R be asymmetric transitive non empty RelStr;

 :: original: DershowitzMannaOrder

 redefine

 :: BAGORD_2:def5

 func DershowitzMannaOrder R means

 : HO: for m,n be Element of it holds m <= n iff m <> n & for a be Element of R st (m . a) > (n . a) holds ex b be Element of R st a <= b & (m . b) < (n . b);

 compatibility

 proof

 let M be strict RelExtension of ( finite-MultiSet_over the carrier of R);

 hereby

 assume

 A1: M = ( DershowitzMannaOrder R);

 let m,n be Element of M;

 hereby

 assume m <= n;

 then

 consider x,y be Element of M such that

 A2: ( 1. M) <> x divides n & m = ((n -' x) + y) & for b be Element of R st (y . b) > 0 holds ex a be Element of R st (x . a) > 0 & b <= a by A1, DM;

 set X = { a where a be Element of R : (x . a) > 0 & ex b be Element of R st (y . b) > 0 & b <= a };



 B1: X c= ( support x)

 proof

 let a;

 assume a in X;

 then

 consider c be Element of R such that

 A3: a = c & (x . c) > 0 & ex b be Element of R st (y . b) > 0 & b <= c;

 thus thesis by A3, PRE_POLY:def 7;

 end;

 x <> y

 proof

 per cases by Th3;

 suppose y = ( 1. M);

 hence thesis by A2;

 end;

 suppose y <> ( 1. ( finite-MultiSet_over the carrier of R));

 then y <> ( EmptyBag the carrier of R) by Th11;

 then

 consider b such that

 A5: b in the carrier of R & (y . b) <> ((the carrier of R --> 0 ) . b) by PBOOLE:def 10;

 reconsider b as Element of R by A5;



 A6: 0 <= (y . b) <> 0 by A5, FUNCOP_1: 7;

 then

 consider a be Element of R such that

 A7: (x . a) > 0 & b <= a by A2;

 a in X by A6, A7;

 then

 consider c be Element of R such that

 A8: c is_maximal_in X by B1, Th12;



 A9: c in X & not ex a be Element of R st a in X & c < a by A8, WAYBEL_4: 55;

 not c in ( support y)

 proof

 assume c in ( support y);

 then

 A11: 0 <= (y . c) <> 0 by PRE_POLY:def 7;

 then

 consider a be Element of R such that

 A12: (x . a) > 0 & c <= a by A2;

 a in X & c < a by A11, A12, Lem2;

 hence contradiction by A8, WAYBEL_4: 55;

 end;

 hence thesis by B1, A9;

 end;

 end;

 hence m <> n by A2, Th9;

 let a be Element of R;

 assume (m . a) > (n . a);

 then ((m . a) - (n . a)) > 0 by XREAL_1: 50;

 then ((m . a) -' (n . a)) > 0 by XREAL_0:def 2;

 then

 A3: ((m -' n) . a) > 0 by PRE_POLY:def 6;

 (m -' n) divides y by A2, Th8;

 then (y . a) > 0 by A3, PRE_POLY:def 11;

 then

 consider b be Element of R such that

 A4: (x . b) > 0 & a <= b by A2;

 set X = { c where c be Element of R : (x . c) > 0 & a <= c };

 X c= ( support x)

 proof

 let b;

 assume b in X;

 then

 consider c be Element of R such that

 B2: b = c & (x . c) > 0 & a <= c;

 thus thesis by B2, PRE_POLY:def 7;

 end;

 then X is finite & b in X by A4;

 then

 consider c be Element of R such that

 B3: c is_maximal_in X by Th12;

 c in X & not ex a be Element of R st a in X & c < a by B3, WAYBEL_4: 55;

 then

 consider d be Element of R such that

 B5: c = d & (x . d) > 0 & a <= d;

 take c;

 thus a <= c by B5;

 assume (m . c) >= (n . c);

 per cases by XXREAL_0: 1;

 suppose (m . c) > (n . c);

 then ((m . c) - (n . c)) > 0 by XREAL_1: 50;

 then ((m . c) -' (n . c)) > 0 & (m -' n) divides y by A2, Th8, XREAL_0:def 2;

 then (y . c) >= ((m -' n) . c) > 0 by PRE_POLY:def 6, PRE_POLY:def 11;

 then

 consider e be Element of R such that

 B6: (x . e) > 0 & c <= e by A2;

 a <= e by B5, B6, YELLOW_0:def 2;

 then e in X & c < e by B6, Lem2;

 hence contradiction by B3, WAYBEL_4: 55;

 end;

 suppose (m . c) = (n . c);

 then (x . c) = ((x . c) -' 0 ) = ((x . c) -' ((n . c) -' (m . c))) = ((x . c) -' ((n -' m) . c)) = ((x -' (n -' m)) . c) = ((y -' (m -' n)) . c) = ((y . c) -' ((m -' n) . c)) = ((y . c) -' ((m . c) -' (n . c))) = ((y . c) -' 0 ) = (y . c) by A2, Th8A, XREAL_1: 232, NAT_D: 40, PRE_POLY:def 6;

 then

 consider e be Element of R such that

 B6: (x . e) > 0 & c <= e by A2, B5;

 a <= e by B5, B6, YELLOW_0:def 2;

 then e in X & c < e by B6, Lem2;

 hence contradiction by B3, WAYBEL_4: 55;

 end;

 end;

 assume

 A5: m <> n & for a be Element of R st (m . a) > (n . a) holds ex b be Element of R st a <= b & (m . b) < (n . b);

 reconsider x = (n -' m), y = (m -' n) as multiset of the carrier of R by Th1;

 reconsider x, y as Element of M by Th2;



 A6: m = ((n -' x) + y) by Th7;



 A8: x divides n by Lem3;

 A9:

 now

 let b be Element of R;

 assume (y . b) > 0 ;

 then ((m . b) -' (n . b)) > 0 by PRE_POLY:def 6;

 then ((m . b) - (n . b)) > 0 by XREAL_0:def 2;

 then

 consider a be Element of R such that

 A7: b <= a & (m . a) < (n . a) by A5, XREAL_1: 47;

 take a;

 ((n . a) - (m . a)) > 0 by A7, XREAL_1: 50;

 then ((n . a) -' (m . a)) > 0 by XREAL_0:def 2;

 hence (x . a) > 0 & b <= a by A7, PRE_POLY:def 6;

 end;

 ( 1. M) <> x

 proof

 per cases by A5, Lem4;

 suppose ( EmptyBag the carrier of R) <> x;

 then ( 1. ( finite-MultiSet_over the carrier of R)) <> x by Th11;

 hence thesis by Th3;

 end;

 suppose ( EmptyBag the carrier of R) <> y;

 then

 consider b such that

 A10: b in the carrier of R & (( EmptyBag the carrier of R) . b) <> (y . b) by PBOOLE:def 10;

 reconsider b as Element of R by A10;

 0 <> (y . b) >= 0 by A10, FUNCOP_1: 7;

 then

 consider a be Element of R such that

 A11: (x . a) > 0 & b <= a by A9;

 take a;

 ( EmptyBag the carrier of R) = ( 1. ( finite-MultiSet_over the carrier of R)) = ( 1. M) by Th11, Th3;

 hence thesis by A11, FUNCOP_1: 7;

 end;

 end;

 hence m <= n by A1, A6, A8, A9, DM;

 end;

 assume

 B1: for m,n be Element of M holds m <= n iff m <> n & for a be Element of R st (m . a) > (n . a) holds ex b be Element of R st a <= b & (m . b) < (n . b);

 for m,n be Element of M holds m <= n iff ex x,y be Element of M st ( 1. M) <> x & x divides n & m = ((n -' x) + y) & for b be Element of R st (y . b) > 0 holds ex a be Element of R st (x . a) > 0 & b <= a

 proof

 let m,n be Element of M;

 hereby

 assume

 Z0: m <= n;

 reconsider x = (n -' m), y = (m -' n) as multiset of the carrier of R by Th1;

 reconsider x, y as Element of M by Th2;

 take x, y;

 A9:

 now

 let b be Element of R;

 assume (y . b) > 0 ;

 then ((m . b) -' (n . b)) > 0 by PRE_POLY:def 6;

 then ((m . b) - (n . b)) > 0 by XREAL_0:def 2;

 then

 consider a be Element of R such that

 A7: b <= a & (m . a) < (n . a) by Z0, B1, XREAL_1: 47;

 take a;

 ((n . a) - (m . a)) > 0 by A7, XREAL_1: 50;

 then ((n . a) -' (m . a)) > 0 by XREAL_0:def 2;

 hence (x . a) > 0 & b <= a by A7, PRE_POLY:def 6;

 end;

 thus ( 1. M) <> x

 proof

 per cases by Z0, B1, Lem4;

 suppose ( EmptyBag the carrier of R) <> x;

 then ( 1. ( finite-MultiSet_over the carrier of R)) <> x by Th11;

 hence thesis by Th3;

 end;

 suppose ( EmptyBag the carrier of R) <> y;

 then

 consider b such that

 A10: b in the carrier of R & (( EmptyBag the carrier of R) . b) <> (y . b) by PBOOLE:def 10;

 reconsider b as Element of R by A10;

 0 <> (y . b) >= 0 by A10, FUNCOP_1: 7;

 then

 consider a be Element of R such that

 A11: (x . a) > 0 & b <= a by A9;

 take a;

 ( EmptyBag the carrier of R) = ( 1. ( finite-MultiSet_over the carrier of R)) = ( 1. M) by Th11, Th3;

 hence thesis by A11, FUNCOP_1: 7;

 end;

 end;

 thus x divides n by Lem3;

 thus m = ((n -' x) + y) by Th7;

 let b be Element of R;

 assume (y . b) > 0 ;

 hence ex a be Element of R st (x . a) > 0 & b <= a by A9;

 end;

 given x,y be Element of M such that

 A2: ( 1. M) <> x & x divides n & m = ((n -' x) + y) & for b be Element of R st (y . b) > 0 holds ex a be Element of R st (x . a) > 0 & b <= a;

 now

 set X = { a where a be Element of R : (x . a) > 0 & ex b be Element of R st (y . b) > 0 & b <= a };



 B1: X c= ( support x)

 proof

 let a;

 assume a in X;

 then

 consider c be Element of R such that

 A3: a = c & (x . c) > 0 & ex b be Element of R st (y . b) > 0 & b <= c;

 thus thesis by A3, PRE_POLY:def 7;

 end;

 x <> y

 proof

 per cases by Th3;

 suppose y = ( 1. M);

 hence thesis by A2;

 end;

 suppose y <> ( 1. ( finite-MultiSet_over the carrier of R));

 then y <> ( EmptyBag the carrier of R) by Th11;

 then

 consider b such that

 A5: b in the carrier of R & (y . b) <> ((the carrier of R --> 0 ) . b) by PBOOLE:def 10;

 reconsider b as Element of R by A5;



 A6: 0 <= (y . b) <> 0 by A5, FUNCOP_1: 7;

 then

 consider a be Element of R such that

 A7: (x . a) > 0 & b <= a by A2;

 a in X by A6, A7;

 then

 consider c be Element of R such that

 A8: c is_maximal_in X by B1, Th12;



 A9: c in X & not ex a be Element of R st a in X & c < a by A8, WAYBEL_4: 55;

 not c in ( support y)

 proof

 assume c in ( support y);

 then

 A11: 0 <= (y . c) <> 0 by PRE_POLY:def 7;

 then

 consider a be Element of R such that

 A12: (x . a) > 0 & c <= a by A2;

 a in X & c < a by A11, A12, Lem2;

 hence contradiction by A8, WAYBEL_4: 55;

 end;

 hence thesis by B1, A9;

 end;

 end;

 hence m <> n by A2, Th9;

 let a be Element of R;

 assume (m . a) > (n . a);

 then ((m . a) - (n . a)) > 0 by XREAL_1: 50;

 then ((m . a) -' (n . a)) > 0 by XREAL_0:def 2;

 then

 A3: ((m -' n) . a) > 0 by PRE_POLY:def 6;

 (m -' n) divides y by A2, Th8;

 then ((m -' n) . a) <= (y . a) by PRE_POLY:def 11;

 then

 consider b be Element of R such that

 A4: (x . b) > 0 & a <= b by A2, A3;

 set X = { c where c be Element of R : (x . c) > 0 & a <= c };

 X c= ( support x)

 proof

 let b;

 assume b in X;

 then

 consider c be Element of R such that

 B2: b = c & (x . c) > 0 & a <= c;

 thus thesis by B2, PRE_POLY:def 7;

 end;

 then X is finite & b in X by A4;

 then

 consider c be Element of R such that

 B3: c is_maximal_in X by Th12;

 c in X & not ex a be Element of R st a in X & c < a by B3, WAYBEL_4: 55;

 then

 consider d be Element of R such that

 B5: c = d & (x . d) > 0 & a <= d;

 take c;

 thus a <= c by B5;

 assume (m . c) >= (n . c);

 per cases by XXREAL_0: 1;

 suppose (m . c) > (n . c);

 then ((m . c) - (n . c)) > 0 by XREAL_1: 50;

 then ((m . c) -' (n . c)) > 0 & (m -' n) divides y by A2, Th8, XREAL_0:def 2;

 then (y . c) >= ((m -' n) . c) > 0 by PRE_POLY:def 6, PRE_POLY:def 11;

 then

 consider e be Element of R such that

 B6: (x . e) > 0 & c <= e by A2;

 a <= e by B5, B6, YELLOW_0:def 2;

 then e in X & c < e by B6, Lem2;

 hence contradiction by B3, WAYBEL_4: 55;

 end;

 suppose (m . c) = (n . c);

 then (x . c) = ((x . c) -' 0 ) = ((x . c) -' ((n . c) -' (m . c))) = ((x . c) -' ((n -' m) . c)) = ((x -' (n -' m)) . c) = ((y -' (m -' n)) . c) = ((y . c) -' ((m -' n) . c)) = ((y . c) -' ((m . c) -' (n . c))) = ((y . c) -' 0 ) = (y . c) by A2, Th8A, XREAL_1: 232, NAT_D: 40, PRE_POLY:def 6;

 then

 consider e be Element of R such that

 B6: (x . e) > 0 & c <= e by A2, B5;

 a <= e by B5, B6, YELLOW_0:def 2;

 then e in X & c < e by B6, Lem2;

 hence contradiction by B3, WAYBEL_4: 55;

 end;

 end;

 hence m <= n by B1;

 end;

 hence M = ( DershowitzMannaOrder R) by DM;

 end;

 end

 theorem :: BAGORD_2:27



 Th15: for k,x1,x2,y1,y2 be bag of I st x2 divides k & x1 divides ((k -' x2) + y2) holds (x2 + (x1 -' y2)) divides k & ((((k -' x2) + y2) -' x1) + y1) = ((k -' (x2 + (x1 -' y2))) + ((y2 -' x1) + y1))

 proof

 let k,x1,x2,y1,y2 be bag of I;

 assume

 A1: for a holds (x2 . a) <= (k . a);

 assume

 A2: for a holds (x1 . a) <= (((k -' x2) + y2) . a);

 hereby

 let a;

 (x2 . a) <= (k . a) & (x1 . a) <= (((k -' x2) + y2) . a) = (((k -' x2) . a) + (y2 . a)) = (((k . a) -' (x2 . a)) + (y2 . a)) by A1, A2, PRE_POLY:def 5, PRE_POLY:def 6;

 then ((x2 . a) + ((x1 . a) -' (y2 . a))) <= (k . a) by Th14;

 then ((x2 . a) + ((x1 -' y2) . a)) <= (k . a) by PRE_POLY:def 6;

 hence ((x2 + (x1 -' y2)) . a) <= (k . a) by PRE_POLY:def 5;

 end;

 let a such that a in I;

 (x2 . a) <= (k . a) & (x1 . a) <= (((k -' x2) + y2) . a) = (((k -' x2) . a) + (y2 . a)) = (((k . a) -' (x2 . a)) + (y2 . a)) by A1, A2, PRE_POLY:def 5, PRE_POLY:def 6;

 then

 A3: (((((k . a) -' (x2 . a)) + (y2 . a)) -' (x1 . a)) + (y1 . a)) = (((k . a) -' ((x2 . a) + ((x1 . a) -' (y2 . a)))) + (((y2 . a) -' (x1 . a)) + (y1 . a))) by Th14;



 A4: (((((k . a) -' (x2 . a)) + (y2 . a)) -' (x1 . a)) + (y1 . a)) = (((((k -' x2) . a) + (y2 . a)) -' (x1 . a)) + (y1 . a)) by PRE_POLY:def 6

 .= (((((k -' x2) + y2) . a) -' (x1 . a)) + (y1 . a)) by PRE_POLY:def 5

 .= (((((k -' x2) + y2) -' x1) . a) + (y1 . a)) by PRE_POLY:def 6

 .= (((((k -' x2) + y2) -' x1) + y1) . a) by PRE_POLY:def 5;

 (((k . a) -' ((x2 . a) + ((x1 . a) -' (y2 . a)))) + (((y2 . a) -' (x1 . a)) + (y1 . a))) = (((k . a) -' ((x2 . a) + ((x1 . a) -' (y2 . a)))) + (((y2 -' x1) . a) + (y1 . a))) by PRE_POLY:def 6

 .= (((k . a) -' ((x2 . a) + ((x1 -' y2) . a))) + (((y2 -' x1) . a) + (y1 . a))) by PRE_POLY:def 6

 .= (((k . a) -' ((x2 + (x1 -' y2)) . a)) + (((y2 -' x1) . a) + (y1 . a))) by PRE_POLY:def 5

 .= (((k . a) -' ((x2 + (x1 -' y2)) . a)) + (((y2 -' x1) + y1) . a)) by PRE_POLY:def 5

 .= (((k -' (x2 + (x1 -' y2))) . a) + (((y2 -' x1) + y1) . a)) by PRE_POLY:def 6;

 hence thesis by A3, A4, PRE_POLY:def 5;

 end;

 registration

 let R be asymmetric transitive non empty RelStr;

 cluster ( DershowitzMannaOrder R) -> asymmetric transitive;

 coherence

 proof

 set DM = ( DershowitzMannaOrder R);

 thus DM is asymmetric

 proof

 let a, b;

 assume a in the carrier of DM & b in the carrier of DM;

 then

 reconsider m = a, n = b as Element of DM;

 assume [a, b] in the InternalRel of DM & [b, a] in the InternalRel of DM;

 then

 A0: m <= n & n <= m by ORDERS_2:def 5;

 then m <> n & (for a be Element of R st (m . a) > (n . a) holds ex b be Element of R st a <= b & (m . b) < (n . b)) & for a be Element of R st (n . a) > (m . a) holds ex b be Element of R st a <= b & (n . b) < (m . b) by HO;

 then

 consider c be object such that

 A2: c in the carrier of R & (m . c) <> (n . c) by PBOOLE:def 10;

 reconsider c as Element of R by A2;

 set X = { d where d be Element of R : c <= d & (m . d) > (n . d) };



 BC: X c= ( support m)

 proof

 let a;

 assume a in X;

 then

 consider d be Element of R such that

 A3: a = d & c <= d & (m . d) > (n . d);

 thus thesis by A3, PRE_POLY:def 7;

 end;

 ex b be Element of R st b in X

 proof

 per cases by A2, XXREAL_0: 1;

 suppose (m . c) < (n . c);

 then

 consider d be Element of R such that

 A5: c <= d & (n . d) < (m . d) by A0, HO;

 take d;

 thus d in X by A5;

 end;

 suppose (m . c) > (n . c);

 then

 consider d be Element of R such that

 A5: c <= d & (n . d) > (m . d) by A0, HO;

 consider e be Element of R such that

 A6: d <= e & (n . e) < (m . e) by A0, HO, A5;

 take e;

 c <= e by A5, A6, ORDERS_2: 3;

 hence e in X by A6;

 end;

 end;

 then

 consider d be Element of R such that

 A7: d is_maximal_in X by BC, Th12;

 d in X & not ex a be Element of R st a in X & d < a by A7, WAYBEL_4: 55;

 then

 consider e be Element of R such that

 A8: d = e & c <= e & (n . e) < (m . e);

 consider f be Element of R such that

 A9: e <= f & (n . f) > (m . f) by A0, HO, A8;

 consider g be Element of R such that

 A10: f <= g & (n . g) < (m . g) by A0, HO, A9;

 c <= f by A8, A9, ORDERS_2: 3;

 then c <= g & d <= g by A8, A9, A10, ORDERS_2: 3;

 then g in X & d < g by A10, Lem2;

 hence contradiction by A7, WAYBEL_4: 55;

 end;

 thus DM is transitive

 proof

 let a,b,c be object;

 assume a in the carrier of DM & b in the carrier of DM & c in the carrier of DM;

 then

 reconsider m = a, n = b, k = c as Element of DM;

 assume [a, b] in the InternalRel of DM & [b, c] in the InternalRel of DM;

 then

 A0: m <= n & n <= k by ORDERS_2:def 5;

 consider x1,y1 be Element of DM such that

 A2: ( 1. DM) <> x1 divides n & m = ((n -' x1) + y1) & for b be Element of R st (y1 . b) > 0 holds ex a be Element of R st (x1 . a) > 0 & b <= a by A0, DM;

 consider x2,y2 be Element of DM such that

 A3: ( 1. DM) <> x2 divides k & n = ((k -' x2) + y2) & for b be Element of R st (y2 . b) > 0 holds ex a be Element of R st (x2 . a) > 0 & b <= a by A0, DM;

 reconsider x = (x2 + (x1 -' y2)), y = ((y2 -' x1) + y1) as multiset of the carrier of R by Th1;

 reconsider x, y as Element of DM by Th2;



 A4: m = ((((k -' x2) + y2) -' x1) + y1) = ((k -' x) + y) by A2, A3, Th15;



 A5: ( 1. DM) <> x

 proof

 consider a such that

 A7: a in the carrier of R & (( 1. DM) . a) <> (x2 . a) by A3, PBOOLE:def 10;

 reconsider a as Element of R by A7;

 ( 1. DM) = ( 1. ( finite-MultiSet_over the carrier of R)) = ( EmptyBag the carrier of R) by Th3, Th11;

 then

 A8: (( 1. DM) . a) = 0 by FUNCOP_1: 7;

 take a;

 0 < (x2 . a) <= ((x2 . a) + ((x1 -' y2) . a)) by A7, A8, NAT_1: 11;

 hence thesis by A8, PRE_POLY:def 5;

 end;



 A6: x divides k by A2, A3, Th15;

 for b be Element of R st (y . b) > 0 holds ex a be Element of R st (x . a) > 0 & b <= a

 proof

 let b be Element of R;

 assume (y . b) > 0 ;

 then (((y2 -' x1) . b) + (y1 . b)) > 0 by PRE_POLY:def 5;

 per cases ;

 suppose ((y2 -' x1) . b) > 0 ;

 then ((y2 . b) -' (x1 . b)) > 0 by PRE_POLY:def 6;

 then ((y2 . b) - (x1 . b)) > 0 by XREAL_0:def 2;

 then (y2 . b) > (x1 . b) >= 0 by XREAL_1: 47;

 then

 consider a be Element of R such that

 B4: (x2 . a) > 0 & b <= a by A3;

 take a;

 (x . a) = ((x2 . a) + ((x1 -' y2) . a)) >= (x2 . a) by NAT_1: 11, PRE_POLY:def 5;

 hence thesis by B4;

 end;

 suppose (y1 . b) > 0 ;

 then

 consider a be Element of R such that

 B1: (x1 . a) > 0 & b <= a by A2;

 per cases ;

 suppose

 B2: ((x1 -' y2) . a) > 0 ;

 take a;

 ((x2 + (x1 -' y2)) . a) = ((x2 . a) + ((x1 -' y2) . a)) by PRE_POLY:def 5;

 hence (x . a) > 0 by B2;

 thus b <= a by B1;

 end;

 suppose ((x1 -' y2) . a) = 0 ;

 then ((x1 . a) -' (y2 . a)) = 0 by PRE_POLY:def 6;

 then (x1 . a) <= (y2 . a) by NAT_D: 36;

 then

 consider c be Element of R such that

 B3: (x2 . c) > 0 & a <= c by A3, B1;

 take c;

 (x . c) = ((x2 . c) + ((x1 -' y2) . c)) by PRE_POLY:def 5;

 hence thesis by B1, B3, ORDERS_2: 3;

 end;

 end;

 end;

 then m <= k by A4, A5, A6, DM;

 hence thesis by ORDERS_2:def 5;

 end;

 end;

 end

 definition

 let I;

 :: BAGORD_2:def6

 func DivOrder I -> Relation of ( Bags I) means

 : DO: for b1,b2 be bag of I holds [b1, b2] in it iff b1 <> b2 & b1 divides b2;

 existence

 proof

 defpred R[ bag of I, bag of I] means $1 <> $2 & $1 divides $2;

 consider R be Relation of ( Bags I) such that

 A1: for b1,b2 be Element of ( Bags I) holds [b1, b2] in R iff R[b1, b2] from RELSET_1:sch 2;

 take R;

 let b1,b2 be bag of I;

 b1 in ( Bags I) & b2 in ( Bags I) by PRE_POLY:def 12;

 hence thesis by A1;

 end;

 uniqueness

 proof

 let R1,R2 be Relation of ( Bags I) such that

 A1: for b1,b2 be bag of I holds [b1, b2] in R1 iff b1 <> b2 & b1 divides b2 and

 A2: for b1,b2 be bag of I holds [b1, b2] in R2 iff b1 <> b2 & b1 divides b2;

 let b1,b2 be Element of ( Bags I);

 [b1, b2] in R1 iff b1 <> b2 & b1 divides b2 by A1;

 hence thesis by A2;

 end;

 end

 theorem :: BAGORD_2:28



 Lem7: for a,b,c be bag of I st a divides b divides c holds a divides c

 proof

 let a,b,c be bag of I;

 assume that

 A1: for x be object holds (a . x) <= (b . x) and

 A2: for x be object holds (b . x) <= (c . x);

 let x be object;

 (a . x) <= (b . x) <= (c . x) by A1, A2;

 hence thesis by XXREAL_0: 2;

 end;

 registration

 let I;

 cluster ( DivOrder I) -> asymmetric transitive;

 coherence

 proof

 set R = ( DivOrder I);

 now

 let x,y be object;

 assume

 A1: [x, y] in R;

 then

 reconsider a = x, b = y as Element of ( Bags I) by ZFMISC_1: 87;



 A2: a <> b & a divides b by DO, A1;

 then

 consider o be object such that

 A3: o in I & (a . o) <> (b . o) by PBOOLE:def 10;

 (a . o) <= (b . o) by A2, PRE_POLY:def 11;

 then (a . o) < (b . o) by A3, XXREAL_0: 1;

 then not b divides a by PRE_POLY:def 11;

 hence not [y, x] in R by DO;

 end;

 hence R is asymmetric by PREFER_1: 22;

 let a,b,c be object;

 assume a in ( field R) & b in ( field R) & c in ( field R);

 assume

 A4: [a, b] in R & [b, c] in R;

 then

 reconsider a, b, c as Element of ( Bags I) by ZFMISC_1: 87;



 A5: a <> b & a divides b & b divides c by A4, DO;

 then

 consider x be object such that

 A6: x in I & (a . x) <> (b . x) by PBOOLE:def 10;

 (a . x) <= (b . x) by A5, PRE_POLY:def 11;

 then (a . x) < (b . x) <= (c . x) by A5, A6, XXREAL_0: 1, PRE_POLY:def 11;

 then a <> c & a divides c by A5, Lem7;

 hence thesis by DO;

 end;

 end

 theorem :: BAGORD_2:29



 Th16: for R be asymmetric transitive non empty RelStr holds ( DivOrder the carrier of R) c= the InternalRel of ( DershowitzMannaOrder R)

 proof

 let R be asymmetric transitive non empty RelStr;

 set DM = ( DershowitzMannaOrder R);

 let a,b be Element of ( Bags the carrier of R);

 assume

 A1: [a, b] in ( DivOrder the carrier of R);

 reconsider a, b as multiset of the carrier of R by Th1;

 reconsider a, b as Element of DM by Th2;



 A2: a <> b & a divides b by A1, DO;

 then for x be Element of R st (a . x) > (b . x) holds ex y be Element of R st x <= y & (a . y) < (b . y) by PRE_POLY:def 11;

 then a <= b by A2, HO;

 hence thesis by ORDERS_2:def 5;

 end;

 theorem :: BAGORD_2:30

 for R be asymmetric transitive non empty RelStr st the InternalRel of R is empty holds the InternalRel of ( DershowitzMannaOrder R) = ( DivOrder the carrier of R)

 proof

 let R be asymmetric transitive non empty RelStr;

 assume

 Z0: the InternalRel of R is empty;

 let a, b;

 hereby

 assume

 A1: [a, b] in the InternalRel of ( DershowitzMannaOrder R);

 then

 reconsider m = a, n = b as Element of ( DershowitzMannaOrder R) by ZFMISC_1: 87;



 A5: m <= n by A1, ORDERS_2:def 5;

 then

 A3: m <> n & for a be Element of R st (m . a) > (n . a) holds ex b be Element of R st a <= b & (m . b) < (n . b) by HO;

 m divides n

 proof

 let a;

 assume

 A4: (m . a) > (n . a);

 a in ( dom m) by A4, FUNCT_1:def 2;

 then

 reconsider a as Element of R;

 consider b be Element of R such that

 A2: a <= b & (m . b) < (n . b) by A5, HO, A4;

 thus thesis by Z0, A2, ORDERS_2:def 5;

 end;

 hence [a, b] in ( DivOrder the carrier of R) by A3, DO;

 end;

 ( DivOrder the carrier of R) c= the InternalRel of ( DershowitzMannaOrder R) by Th16;

 hence thesis;

 end;

 theorem :: BAGORD_2:31

 for R1,R2 be asymmetric transitive non empty RelStr st the carrier of R1 = the carrier of R2 & the InternalRel of R1 c= the InternalRel of R2 holds the InternalRel of ( DershowitzMannaOrder R1) c= the InternalRel of ( DershowitzMannaOrder R2)

 proof

 let R1,R2 be asymmetric transitive non empty RelStr;

 assume

 Z0: the carrier of R1 = the carrier of R2 & the InternalRel of R1 c= the InternalRel of R2;

 let a,b be Element of ( DershowitzMannaOrder R1);

 assume [a, b] in the InternalRel of ( DershowitzMannaOrder R1);

 then

 A3: a <= b by ORDERS_2:def 5;

 then

 A1: a <> b & for x be Element of R1 st (a . x) > (b . x) holds ex y be Element of R1 st x <= y & (a . y) < (b . y) by HO;

 reconsider b1 = b, a1 = a as multiset of the carrier of R1 by Th1;

 reconsider b1, a1 as Element of ( DershowitzMannaOrder R2) by Z0, Th2;

 now

 let x be Element of R2;

 reconsider x1 = x as Element of R1 by Z0;

 assume (a1 . x) > (b1 . x);

 then

 consider y be Element of R1 such that

 A2: x1 <= y & (a . y) < (b . y) by A3, HO;

 reconsider y1 = y as Element of R2 by Z0;

 take y1;

 [x1, y] in the InternalRel of R1 by A2, ORDERS_2:def 5;

 hence x <= y1 & (a1 . y1) < (b1 . y1) by Z0, A2, ORDERS_2:def 5;

 end;

 then a1 <= b1 by A1, HO;

 hence thesis by ORDERS_2:def 5;

 end;

 begin

 definition

 let I;

 let f be ( Bags I) -valued FinSequence;

 :: BAGORD_2:def7

 func Sum f -> bag of I means

 : SUM: ex F be Function of NAT , ( Bags I) st it = (F . ( len f)) & (F . 0 ) = ( EmptyBag I) & for i be Nat holds for b be bag of I st i < ( len f) & b = (f . (i + 1)) holds (F . (i + 1)) = ((F . i) + b);

 existence

 proof

 defpred P[ set] means for F be ( Bags I) -valued FinSequence st ( len F) = $1 holds ex u be bag of I st ex f be Function of NAT , ( Bags I) st u = (f . ( len F)) & (f . 0 ) = ( EmptyBag I) & for j be Nat, v be bag of I st j < ( len F) & v = (F . (j + 1)) holds (f . (j + 1)) = ((f . j) + v);

 set V = ( Bags I);



 A1: for n be Nat st P[n] holds P[(n + 1)]

 proof

 let n be Nat;

 assume

 A2: P[n];

 let F be ( Bags I) -valued FinSequence;



 A3: ( rng F) c= ( Bags I) by RELAT_1:def 19;

 then

 reconsider F1 = F as FinSequence of V by FINSEQ_1:def 4;

 reconsider G = (F1 | ( Seg n)) as FinSequence of V by FINSEQ_1: 18;

 assume

 A4: ( len F) = (n + 1);

 then ( dom F) = ( Seg (n + 1)) by FINSEQ_1:def 3;

 then (n + 1) in ( dom F) by FINSEQ_1: 4;

 then (F . (n + 1)) in ( rng F) by FUNCT_1:def 3;

 then

 reconsider u1 = (F . (n + 1)) as Element of V by A3;



 A5: n < (n + 1) by NAT_1: 13;

 then

 consider u be bag of I, f be Function of NAT , V such that u = (f . ( len G)) and

 A6: (f . 0 ) = ( EmptyBag I) and

 A7: for j be Nat, v be bag of I st j < ( len G) & v = (G . (j + 1)) holds (f . (j + 1)) = ((f . j) + v) by A2, A4, FINSEQ_1: 17;

 defpred P[ set, set] means for j be Nat st $1 = j holds (j < (n + 1) implies $2 = (f . $1)) & ((n + 1) <= j implies for u be bag of I st u = (F . (n + 1)) holds $2 = ((f . ( len G)) + u));



 A8: for k be Element of NAT holds ex v be Element of V st P[k, v]

 proof

 let k be Element of NAT ;

 reconsider i = k as Element of NAT ;

 A9:

 now

 assume

 A10: (n + 1) <= i;

 take v = ((f . ( len G)) + u1);

 let j be Nat;

 assume k = j;

 hence j < (n + 1) implies v = (f . k) by A10;

 assume (n + 1) <= j;

 let u2 be bag of I;

 assume u2 = (F . (n + 1));

 hence v = ((f . ( len G)) + u2);

 end;

 now

 assume

 A11: i < (n + 1);

 take v = (f . k);

 let j be Nat such that

 A12: k = j;

 thus j < (n + 1) implies v = (f . k);

 thus (n + 1) <= j implies for u be bag of I st u = (F . (n + 1)) holds v = ((f . ( len G)) + u) by A11, A12;

 end;

 then

 consider v be bag of I such that

 B13: P[k, v] by A9;

 v in V by PRE_POLY:def 12;

 hence thesis by B13;

 end;

 consider f9 be sequence of ( Bags I) such that

 A13: for k be Element of NAT holds P[k, (f9 . k)] from FUNCT_2:sch 3( A8);



 A14: for k be Nat holds P[k, (f9 . k)]

 proof

 let k be Nat;

 k in NAT by ORDINAL1:def 12;

 hence thesis by A13;

 end;

 take z = (f9 . (n + 1));

 take f99 = f9;

 thus z = (f99 . ( len F)) by A4;

 thus (f99 . 0 ) = ( EmptyBag I) by A6, A14;

 let j be Nat, v be bag of I;

 assume that

 A15: j < ( len F) and

 A16: v = (F . (j + 1));



 A17: ( len G) = n by A4, A5, FINSEQ_1: 17;

 A18:

 now

 assume

 A19: j = n;

 then (f99 . (j + 1)) = ((f . j) + v) by A17, A14, A16;

 hence (f99 . (j + 1)) = ((f99 . j) + v) by A5, A14, A19;

 end;

 A20:

 now

 assume

 A21: j < n;

 then

 A22: (j + 1) < (n + 1) by XREAL_1: 6;

 1 <= (1 + j) & (j + 1) <= n by A21, NAT_1: 11, NAT_1: 13;

 then (j + 1) in ( Seg n);

 then

 A23: v = (G . (j + 1)) by A16, FUNCT_1: 49;

 j < ( len G) by A4, A5, A21, FINSEQ_1: 17;

 then

 A24: (f . (j + 1)) = ((f . j) + v) by A7, A23;

 j < (n + 1) by A21, NAT_1: 13;

 then (f . (j + 1)) = ((f9 . j) + v) by A14, A24;

 hence (f99 . (j + 1)) = ((f99 . j) + v) by A14, A22;

 end;

 j <= n by A4, A15, NAT_1: 13;

 hence (f99 . (j + 1)) = ((f99 . j) + v) by A20, A18, XXREAL_0: 1;

 end;



 A25: P[ 0 ]

 proof

 reconsider f = ( NAT --> ( EmptyBag I)) as sequence of ( Bags I);

 let F be ( Bags I) -valued FinSequence;

 assume

 A26: ( len F) = 0 ;

 take u = (f . ( len F));

 take f9 = f;

 thus u = (f9 . ( len F)) & (f9 . 0 ) = ( EmptyBag I) by FUNCOP_1: 7;

 let j be Nat;

 let v be bag of I;

 thus j < ( len F) & v = (F . (j + 1)) implies (f9 . (j + 1)) = ((f9 . j) + v) by A26;

 end;

 for n be Nat holds P[n] from NAT_1:sch 2( A25, A1);

 hence thesis;

 end;

 uniqueness

 proof

 let v1,v2 be bag of I;

 given F be Function of NAT , ( Bags I) such that

 A27: v1 = (F . ( len f)) and

 A28: (F . 0 ) = ( EmptyBag I) and

 A29: for j be Nat, v be bag of I st j < ( len f) & v = (f . (j + 1)) holds (F . (j + 1)) = ((F . j) + v);

 given f9 be Function of NAT , ( Bags I) such that

 A30: v2 = (f9 . ( len f)) and

 A31: (f9 . 0 ) = ( EmptyBag I) and

 A32: for j be Nat, v be bag of I st j < ( len f) & v = (f . (j + 1)) holds (f9 . (j + 1)) = ((f9 . j) + v);

 defpred P[ Nat] means $1 <= ( len f) implies (F . $1) = (f9 . $1);

 now



 A33: ( rng f) c= ( Bags I) by RELAT_1:def 19;

 let k be Nat;

 assume

 A34: P[k];

 assume

 A35: (k + 1) <= ( len f);

 1 <= (k + 1) & ( dom f) = ( Seg ( len f)) by FINSEQ_1:def 3, NAT_1: 11;

 then (k + 1) in ( dom f) by A35;

 then (f . (k + 1)) in ( rng f) by FUNCT_1:def 3;

 then

 reconsider u1 = (f . (k + 1)) as Element of ( Bags I) by A33;

 (F . (k + 1)) = ((F . k) + u1) by A29, A35, NAT_1: 13;

 hence (F . (k + 1)) = (f9 . (k + 1)) by A32, A34, A35, NAT_1: 13;

 end;

 then

 A37: for k be Nat st P[k] holds P[(k + 1)];



 A38: P[ 0 ] by A28, A31;

 for k be Nat holds P[k] from NAT_1:sch 2( A38, A37);

 hence thesis by A27, A30;

 end;

 end

 theorem :: BAGORD_2:32



 Th21: ( Sum ( <*> ( Bags I))) = ( EmptyBag I)

 proof

 set f = ( <*> ( Bags I));

 consider F be Function of NAT , ( Bags I) such that

 A1: ( Sum f) = (F . ( len f)) and

 A2: (F . 0 ) = ( EmptyBag I) and for i be Nat holds for b be bag of I st i < ( len f) & b = (f . (i + 1)) holds (F . (i + 1)) = ((F . i) + b) by SUM;

 thus thesis by A1, A2;

 end;

 registration

 let I;

 let b be bag of I;

 cluster <*b*> -> ( Bags I) -valued;

 coherence

 proof

 ( rng <*b*>) = {b} & b in ( Bags I) by PRE_POLY:def 12, FINSEQ_1: 39;

 hence thesis by RELAT_1:def 19, ZFMISC_1: 31;

 end;

 end

 theorem :: BAGORD_2:33



 Th22: for p be ( Bags I) -valued FinSequence, b be bag of I holds ( Sum (p ^ <*b*>)) = (( Sum p) + b)

 proof

 let p be ( Bags I) -valued FinSequence;

 let b be bag of I;

 set f = (p ^ <*b*>);

 consider F be Function of NAT , ( Bags I) such that

 A1: ( Sum f) = (F . ( len f)) and

 A2: (F . 0 ) = ( EmptyBag I) and

 A3: for i be Nat holds for b be bag of I st i < ( len f) & b = (f . (i + 1)) holds (F . (i + 1)) = ((F . i) + b) by SUM;

 consider F1 be Function of NAT , ( Bags I) such that

 A4: ( Sum p) = (F1 . ( len p)) and

 A5: (F1 . 0 ) = ( EmptyBag I) and

 A6: for i be Nat holds for b be bag of I st i < ( len p) & b = (p . (i + 1)) holds (F1 . (i + 1)) = ((F1 . i) + b) by SUM;

 defpred P[ Nat] means $1 <= ( len p) implies (F . $1) = (F1 . $1);



 A7: P[ 0 ] by A2, A5;



 A8: for i be Nat st P[i] holds P[(i + 1)]

 proof

 let i be Nat;

 assume

 A9: P[i] & (i + 1) <= ( len p);

 then i < ( len p) < (( len p) + 1) = ( len f) by FINSEQ_2: 16, NAT_1: 13;

 then

 A11: i < ( len f) by XXREAL_0: 2;



 A12: (i + 1) in ( dom p) by A9, NAT_1: 11, FINSEQ_3: 25;

 then

 reconsider b = (p . (i + 1)) as Element of ( Bags I) by FUNCT_1: 102;

 (f . (i + 1)) = b by A12, FINSEQ_1:def 7;



 hence (F . (i + 1)) = ((F . i) + b) by A3, A11

 .= ((F1 . i) + b) by A9, NAT_1: 13

 .= (F1 . (i + 1)) by A6, A9, NAT_1: 13;

 end;

 for i be Nat holds P[i] from NAT_1:sch 2( A7, A8);

 then ( Sum p) = (F . ( len p)) & ( len p) < (( len p) + 1) = ( len f) & (f . (( len p) + 1)) = b by A4, NAT_1: 13, FINSEQ_2: 16, FINSEQ_1: 42;

 hence ( Sum (p ^ <*b*>)) = (( Sum p) + b) by A1, A3;

 end;

 reserve b for bag of I;

 theorem :: BAGORD_2:34



 Th23: ( Sum <*b*>) = b

 proof



 thus ( Sum <*b*>) = ( Sum (( <*> ( Bags I)) ^ <*b*>)) by FINSEQ_1: 34

 .= (( Sum ( <*> ( Bags I))) + b) by Th22

 .= (( EmptyBag I) + b) by Th21

 .= b by PRE_POLY: 53;

 end;

 theorem :: BAGORD_2:35



 Th24: for p,q be ( Bags I) -valued FinSequence holds ( Sum (p ^ q)) = (( Sum p) + ( Sum q))

 proof

 let p,q be ( Bags I) -valued FinSequence;

 set f = (p ^ q);

 consider F be Function of NAT , ( Bags I) such that

 A1: ( Sum f) = (F . ( len f)) and

 A2: (F . 0 ) = ( EmptyBag I) and

 A3: for i be Nat holds for b be bag of I st i < ( len f) & b = (f . (i + 1)) holds (F . (i + 1)) = ((F . i) + b) by SUM;

 consider F1 be Function of NAT , ( Bags I) such that

 A4: ( Sum p) = (F1 . ( len p)) and

 A5: (F1 . 0 ) = ( EmptyBag I) and

 A6: for i be Nat holds for b be bag of I st i < ( len p) & b = (p . (i + 1)) holds (F1 . (i + 1)) = ((F1 . i) + b) by SUM;

 consider F2 be Function of NAT , ( Bags I) such that

 B1: ( Sum q) = (F2 . ( len q)) and

 B2: (F2 . 0 ) = ( EmptyBag I) and

 B3: for i be Nat holds for b be bag of I st i < ( len q) & b = (q . (i + 1)) holds (F2 . (i + 1)) = ((F2 . i) + b) by SUM;

 defpred P[ Nat] means $1 <= ( len p) implies (F . $1) = (F1 . $1);



 A7: P[ 0 ] by A2, A5;



 A8: for i be Nat st P[i] holds P[(i + 1)]

 proof

 let i be Nat;

 assume

 A9: P[i] & (i + 1) <= ( len p);

 then i < ( len p) <= (( len p) + ( len q)) = ( len f) by FINSEQ_1: 22, NAT_1: 11, NAT_1: 13;

 then

 A11: i < ( len f) by XXREAL_0: 2;



 A12: (i + 1) in ( dom p) by A9, NAT_1: 11, FINSEQ_3: 25;

 then

 reconsider b = (p . (i + 1)) as Element of ( Bags I) by FUNCT_1: 102;

 (f . (i + 1)) = b by A12, FINSEQ_1:def 7;



 hence (F . (i + 1)) = ((F . i) + b) by A3, A11

 .= ((F1 . i) + b) by A9, NAT_1: 13

 .= (F1 . (i + 1)) by A6, A9, NAT_1: 13;

 end;

 for i be Nat holds P[i] from NAT_1:sch 2( A7, A8);

 then

 A13: ( Sum p) = (F . ( len p)) by A4;

 defpred Q[ Nat] means $1 <= ( len q) implies (F . (( len p) + $1)) = (( Sum p) + (F2 . $1));



 A14: Q[ 0 ] by A13, B2, PRE_POLY: 53;



 A15: for i be Nat st Q[i] holds Q[(i + 1)]

 proof

 let i be Nat;

 assume

 A9: Q[i] & (i + 1) <= ( len q);

 then

 A10: i < ( len q) & (( len p) + ( len q)) = ( len f) by FINSEQ_1: 22, NAT_1: 13;



 A12: (i + 1) in ( dom q) by A9, NAT_1: 11, FINSEQ_3: 25;

 then

 reconsider b = (q . (i + 1)) as Element of ( Bags I) by FUNCT_1: 102;

 reconsider lp = ( len p) as Nat;

 reconsider lpi = (lp + i) as Nat;

 (f . (( len p) + (i + 1))) = b & (( len p) + (i + 1)) = ((( len p) + i) + 1) by A12, FINSEQ_1:def 7;



 hence (F . (( len p) + (i + 1))) = ((F . lpi) + b) by A3, A10, XREAL_1: 6

 .= ((( Sum p) + (F2 . i)) + b) by A9, NAT_1: 13

 .= (( Sum p) + ((F2 . i) + b)) by RFUNCT_1: 8

 .= (( Sum p) + (F2 . (i + 1))) by B3, A9, NAT_1: 13;

 end;

 for i be Nat holds Q[i] from NAT_1:sch 2( A14, A15);

 then (F . (( len p) + ( len q))) = (( Sum p) + ( Sum q)) by B1;

 hence ( Sum (p ^ q)) = (( Sum p) + ( Sum q)) by A1, FINSEQ_1: 22;

 end;

 theorem :: BAGORD_2:36



 Th25: for p be ( Bags I) -valued FinSequence holds ( Sum ( <*b*> ^ p)) = (b + ( Sum p))

 proof

 let p be ( Bags I) -valued FinSequence;



 thus ( Sum ( <*b*> ^ p)) = (( Sum <*b*>) + ( Sum p)) by Th24

 .= (b + ( Sum p)) by Th23;

 end;

 theorem :: BAGORD_2:37



 Th26: for p be ( Bags I) -valued FinSequence st b in ( rng p) holds b divides ( Sum p)

 proof

 let p be ( Bags I) -valued FinSequence;

 assume b in ( rng p);

 then

 consider q,r be FinSequence such that

 A1: p = ((q ^ <*b*>) ^ r) by Lem9;

 reconsider qb = (q ^ <*b*>), r as ( Bags I) -valued FinSequence by A1, Lem8;

 qb = qb;

 then

 reconsider q as ( Bags I) -valued FinSequence by Lem8;

 ( Sum p) = (( Sum (q ^ <*b*>)) + ( Sum r)) = ((( Sum q) + b) + ( Sum r)) = ((( Sum r) + ( Sum q)) + b) by A1, Th22, Th24, RFUNCT_1: 8;

 hence b divides ( Sum p) by PRE_POLY: 50;

 end;

 theorem :: BAGORD_2:38



 Th27: for p be ( Bags I) -valued FinSequence, i be object st i in ( support ( Sum p)) holds ex b st b in ( rng p) & i in ( support b)

 proof

 defpred P[ Nat] means for p be ( Bags I) -valued FinSequence st ( len p) = $1 holds for i be object st i in ( support ( Sum p)) holds ex b st b in ( rng p) & i in ( support b);



 A1: P[ 0 ]

 proof

 let p be ( Bags I) -valued FinSequence such that

 A2: ( len p) = 0 ;

 let i be object;

 assume

 Z0: i in ( support ( Sum p));

 p = {} = ( <*> ( Bags I)) by A2;

 then i in ( support ( EmptyBag I)) by Z0, Th21;

 hence thesis;

 end;



 A3: for j be Nat st P[j] holds P[(j + 1)]

 proof

 let j be Nat;

 assume

 A4: P[j];

 let p be ( Bags I) -valued FinSequence such that

 A2: ( len p) = (j + 1);

 consider w be FinSequence, x be set such that

 A5: p = (w ^ <*x*>) & ( len w) = j by A2, TREES_2: 3;

 reconsider w, xx = <*x*> as ( Bags I) -valued FinSequence by A5, Lem8;

 ( len xx) = 1 by FINSEQ_1: 40;

 then 1 in ( dom xx) by FINSEQ_3: 25;

 then x = (xx . 1) in ( Bags I) by FUNCT_1: 102, FINSEQ_1: 40;

 then

 reconsider x as Element of ( Bags I);

 ( Sum p) = (( Sum w) + x) by A5, Th22;

 then

 A6: ( support ( Sum p)) = (( support ( Sum w)) \/ ( support x)) by PRE_POLY: 38;

 let i be object;

 assume i in ( support ( Sum p));

 per cases by A6, XBOOLE_0:def 3;

 suppose i in ( support ( Sum w));

 then

 consider b such that

 A7: b in ( rng w) & i in ( support b) by A4, A5;

 take b;

 ( rng p) = (( rng w) \/ ( rng xx)) by A5, FINSEQ_1: 31;

 hence thesis by A7, XBOOLE_0:def 3;

 end;

 suppose

 A8: i in ( support x);

 take b = x;

 ( rng p) = (( rng w) \/ ( rng xx)) & x in {x} = ( rng xx) by A5, FINSEQ_1: 31, FINSEQ_1: 39, TARSKI:def 1;

 hence thesis by A8, XBOOLE_0:def 3;

 end;

 end;

 let p be ( Bags I) -valued FinSequence;

 for j be Nat holds P[j] from NAT_1:sch 2( A1, A3);

 then P[( len p)];

 hence thesis;

 end;

 definition

 let I, b;

 :: BAGORD_2:def8

 mode partition of b -> ( Bags I) -valued FinSequence means

 : PART: b = ( Sum it );

 existence

 proof

 take <*b*>;

 thus thesis by Th23;

 end;

 end

 definition

 let I, b;

 :: original: <*

 redefine

 func <*b*> -> partition of b ;

 coherence

 proof

 thus b = ( Sum <*b*>) by Th23;

 end;

 end

 definition

 let R be RelStr;

 let M be RelExtension of ( finite-MultiSet_over the carrier of R);

 let b be Element of M;

 let p be partition of b;

 :: BAGORD_2:def9

 attr p is co-ordered means for i be Nat st i in ( dom p) & (i + 1) in ( dom p) holds for b1,b2 be Element of M st b1 = (p . i) & b2 = (p . (i + 1)) holds b2 <= b1;

 end

 definition

 let R be non empty RelStr;

 let b be bag of the carrier of R;

 let p be partition of b;

 :: BAGORD_2:def10

 attr p is ordered means (for m be bag of the carrier of R st m in ( rng p) holds for x be Element of R st (m . x) > 0 holds (m . x) = (b . x)) & (for m be bag of the carrier of R st m in ( rng p) holds for x,y be Element of R st (m . x) > 0 & (m . y) > 0 & x <> y holds x ## y) & (for m be bag of the carrier of R st m in ( rng p) holds m <> ( EmptyBag the carrier of R)) & (for i be Nat st i in ( dom p) & (i + 1) in ( dom p) holds for x be Element of R st ((p /. (i + 1)) . x) > 0 holds ex y be Element of R st ((p /. i) . y) > 0 & x <= y);

 end

 reserve R for asymmetric transitive non empty RelStr,

a,b,c for bag of the carrier of R,

x,y,z for Element of R;

 theorem :: BAGORD_2:39

 <*a*> is ordered iff a <> ( EmptyBag the carrier of R) & for x, y st (a . x) > 0 & (a . y) > 0 & x <> y holds x ## y

 proof

 hereby

 assume

 Z0: <*a*> is ordered;

 a in {a} = ( rng <*a*>) by TARSKI:def 1, FINSEQ_1: 39;

 hence a <> ( EmptyBag the carrier of R) & for x, y st (a . x) > 0 & (a . y) > 0 & x <> y holds x ## y by Z0;

 end;

 assume

 Z3: a <> ( EmptyBag the carrier of R);

 assume

 Z4: for x, y st (a . x) > 0 & (a . y) > 0 & x <> y holds x ## y;

 set p = <*a*>;

 hereby

 let m be bag of the carrier of R;

 assume m in ( rng p);

 then m in {a} by FINSEQ_1: 39;

 hence for x be Element of R st (m . x) > 0 holds (m . x) = (a . x) by TARSKI:def 1;

 end;

 hereby

 let m be bag of the carrier of R;

 assume m in ( rng p);

 then m in {a} by FINSEQ_1: 39;

 then m = a by TARSKI:def 1;

 hence for x,y be Element of R st (m . x) > 0 & (m . y) > 0 & x <> y holds x ## y by Z4;

 end;

 hereby

 let m be bag of the carrier of R;

 assume m in ( rng p);

 then m in {a} by FINSEQ_1: 39;

 hence m <> ( EmptyBag the carrier of R) by Z3, TARSKI:def 1;

 end;

 let i be Nat;

 assume i in ( dom p) & (i + 1) in ( dom p);

 then 1 <= i < (i + 1) <= ( len p) = 1 by FINSEQ_1: 40, FINSEQ_3: 25, NAT_1: 13;

 hence thesis by XXREAL_0: 2;

 end;

 theorem :: BAGORD_2:40



 Th28: for p be ( Bags I) -valued FinSequence holds for a,b be bag of I holds ( <*a*> ^ p) is partition of b iff a divides b & p is partition of (b -' a)

 proof

 let p be ( Bags I) -valued FinSequence;

 let a,b be bag of I;

 thus ( <*a*> ^ p) is partition of b implies a divides b & p is partition of (b -' a)

 proof

 assume b = ( Sum ( <*a*> ^ p));

 then

 A1: b = (a + ( Sum p)) by Th25;

 hence a divides b by PRE_POLY: 50;

 thus (b -' a) = ( Sum p) by A1, PRE_POLY: 48;

 end;

 assume

 Z1: a divides b;

 assume (b -' a) = ( Sum p);

 then (( Sum p) + a) = ((b -' a) + a) = b by Z1, PRE_POLY: 47;

 hence b = ( Sum ( <*a*> ^ p)) by Th25;

 end;

 reserve p for partition of (b -' a),

q for partition of b;

 theorem :: BAGORD_2:41



 Th30: q = ( <*a*> ^ p) & q is ordered implies p is ordered

 proof

 assume

 Z1: q = ( <*a*> ^ p);

 assume

 Z2: q is ordered;

 hereby

 let m be bag of the carrier of R;

 assume

 A0: m in ( rng p);

 then

 A1: m in (( rng <*a*>) \/ ( rng p)) = ( rng q) by Z1, XBOOLE_0:def 3, FINSEQ_1: 31;

 let x be Element of R;

 assume

 A2: (m . x) > 0 ;

 m divides ( Sum p) = (b -' a) divides b by A0, Th26, PART, Lem3;

 then (b . x) = (m . x) <= ((b -' a) . x) <= (b . x) by A1, A2, Z2, PRE_POLY:def 11;

 hence (m . x) = ((b -' a) . x) by XXREAL_0: 1;

 end;

 hereby

 let m be bag of the carrier of R;

 assume m in ( rng p);

 then m in (( rng <*a*>) \/ ( rng p)) = ( rng q) by Z1, FINSEQ_1: 31, XBOOLE_0:def 3;

 hence for x,y be Element of R st (m . x) > 0 & (m . y) > 0 & x <> y holds x ## y by Z2;

 end;

 hereby

 let m be bag of the carrier of R;

 assume m in ( rng p);

 then m in (( rng <*a*>) \/ ( rng p)) = ( rng q) by Z1, FINSEQ_1: 31, XBOOLE_0:def 3;

 hence m <> ( EmptyBag the carrier of R) by Z2;

 end;

 let i be Nat;

 assume

 A1: i in ( dom p) & (i + 1) in ( dom p);



 A2: ( len <*a*>) = 1 by FINSEQ_1: 40;

 then

 A3: (q . (1 + i)) = (p . i) & (q . (1 + (i + 1))) = (p . (i + 1)) by Z1, A1, FINSEQ_1:def 7;



 A4: (1 + i) in ( dom q) & ((1 + i) + 1) = (1 + (i + 1)) in ( dom q) by Z1, A1, A2, FINSEQ_1: 28;

 then (q . (1 + i)) = (q /. (1 + i)) & (p /. i) = (p . i) & (q . (1 + (i + 1))) = (q /. ((1 + i) + 1)) & (p . (i + 1)) = (p /. (i + 1)) by A1, PARTFUN1:def 6;

 hence thesis by Z2, A3, A4;

 end;

 definition

 let I;

 let m be bag of I;

 let J be set;

 :: BAGORD_2:def11

 func m | J -> bag of I means

 : BAR: for i be object st i in I holds (i in J implies (it . i) = (m . i)) & ( not i in J implies (it . i) = 0 );

 existence

 proof

 defpred C[ object] means $1 in J;

 deffunc F( object) = (m . $1);

 deffunc G( object) = 0 ;

 consider f be Function such that

 A1: ( dom f) = I & for x be object st x in I holds ( C[x] implies (f . x) = F(x)) & ( not C[x] implies (f . x) = G(x)) from PARTFUN1:sch 1;

 ( rng f) c= NAT

 proof

 let x be object;

 assume x in ( rng f);

 then

 consider i be object such that

 A2: i in ( dom f) & x = (f . i) by FUNCT_1:def 3;

 x = F(i) or x = G(i) by A1, A2;

 hence thesis by ORDINAL1:def 12;

 end;

 then

 reconsider f as Function of I, NAT by A1, FUNCT_2: 2;

 f is finite-support

 proof

 ( support f) c= ( support m)

 proof

 let x be object;

 assume x in ( support f);

 then

 A3: (f . x) <> 0 by PRE_POLY:def 7;

 then x in ( dom f) by FUNCT_1:def 2;

 then (f . x) = (m . x) by A1, A3;

 hence thesis by A3, PRE_POLY:def 7;

 end;

 hence ( support f) is finite;

 end;

 then

 reconsider f as bag of I;

 take f;

 thus thesis by A1;

 end;

 uniqueness

 proof

 let b1,b2 be bag of I such that

 A1: for i be object st i in I holds (i in J implies (b1 . i) = (m . i)) & ( not i in J implies (b1 . i) = 0 ) and

 A2: for i be object st i in I holds (i in J implies (b2 . i) = (m . i)) & ( not i in J implies (b2 . i) = 0 );

 let i be object;

 assume

 A3: i in I;

 per cases ;

 suppose i in J;

 then (b1 . i) = (m . i) = (b2 . i) by A1, A2, A3;

 hence thesis;

 end;

 suppose not i in J;

 then (b1 . i) = 0 = (b2 . i) by A1, A2, A3;

 hence thesis;

 end;

 end;

 end

 reserve J for set,

m for bag of I;

 theorem :: BAGORD_2:42



 Th44: ( support (m | J)) = (J /\ ( support m))

 proof

 set f = (m | J);

 thus ( support f) c= (J /\ ( support m))

 proof

 let x be object;

 assume x in ( support f);

 then

 A3: (f . x) <> 0 by PRE_POLY:def 7;

 then

 A4: x in ( dom f) = I by PARTFUN1:def 2, FUNCT_1:def 2;

 then

 A5: x in J by BAR, A3;

 then (f . x) = (m . x) by BAR, A4;

 then x in ( support m) by A3, PRE_POLY:def 7;

 hence thesis by A5, XBOOLE_0:def 4;

 end;

 let x be object;

 assume x in (J /\ ( support m));

 then

 A1: x in J & x in ( support m) by XBOOLE_0:def 4;

 then

 A2: (m . x) <> 0 by PRE_POLY:def 7;

 then x in ( dom m) = I by PARTFUN1:def 2, FUNCT_1:def 2;

 then (f . x) = (m . x) by A1, BAR;

 hence thesis by A2, PRE_POLY:def 7;

 end;

 theorem :: BAGORD_2:43

 ((m | J) + (m | (I \ J))) = m

 proof

 let i be object;

 assume

 A1: i in I;



 A3: (((m | J) + (m | (I \ J))) . i) = (((m | J) . i) + ((m | (I \ J)) . i)) by PRE_POLY:def 5;

 per cases ;

 suppose

 A2: i in J;

 then not i in (I \ J) by XBOOLE_0:def 5;

 then ((m | J) . i) = (m . i) & ((m | (I \ J)) . i) = 0 by A1, A2, BAR;

 hence thesis by A3;

 end;

 suppose

 A2: not i in J;

 then i in (I \ J) by A1, XBOOLE_0:def 5;

 then ((m | J) . i) = 0 & ((m | (I \ J)) . i) = (m . i) by A2, BAR;

 hence thesis by A3;

 end;

 end;

 theorem :: BAGORD_2:44



 Th43: (m | J) divides m

 proof

 let i be object;

 per cases ;

 suppose

 A1: not i in I;

 ( dom (m | J)) = I & ( dom m) = I by PARTFUN1:def 2;

 hence thesis by A1, FUNCT_1:def 2;

 end;

 suppose

 A2: i in I;

 per cases ;

 suppose i in J;

 hence thesis by A2, BAR;

 end;

 suppose not i in J;

 hence thesis by A2, BAR;

 end;

 end;

 end;

 theorem :: BAGORD_2:45

 ( support m) c= J implies (m | J) = m

 proof

 assume

 A1: ( support m) c= J;

 let i be object;

 assume

 A2: i in I;

 per cases ;

 suppose i in J;

 hence thesis by A2, BAR;

 end;

 suppose not i in J;

 then ((m | J) . i) = 0 & not i in ( support m) by A1, A2, BAR;

 hence thesis by PRE_POLY:def 7;

 end;

 end;

 theorem :: BAGORD_2:46



 Th27A: ( support (m -' (m | J))) = (( support m) \ J)

 proof

 thus ( support (m -' (m | J))) c= (( support m) \ J)

 proof

 let x be object;

 assume x in ( support (m -' (m | J)));

 then ((m -' (m | J)) . x) <> 0 by PRE_POLY:def 7;

 then ((m . x) -' ((m | J) . x)) <> 0 by PRE_POLY:def 6;

 then ((m . x) -' ((m | J) . x)) > 0 ;

 then ((m . x) - ((m | J) . x)) > 0 by XREAL_0:def 2;

 then (m . x) > ((m | J) . x) by XREAL_1: 47;

 then (m . x) <> ((m | J) . x) & x in ( dom m) = I & (m . x) > 0 by PARTFUN1:def 2, FUNCT_1:def 2;

 then not x in J & x in ( support m) by BAR, PRE_POLY:def 7;

 hence x in (( support m) \ J) by XBOOLE_0:def 5;

 end;

 let x be object;

 assume x in (( support m) \ J);

 then

 A1: x in ( support m) & not x in J by XBOOLE_0:def 5;

 then

 A2: (m . x) <> 0 by PRE_POLY:def 7;

 then x in ( dom m) = I by PARTFUN1:def 2, FUNCT_1:def 2;

 then ((m | J) . x) = 0 by A1, BAR;

 then ((m -' (m | J)) . x) = ((m . x) -' ((m | J) . x)) <> 0 by A2, NAT_D: 40, PRE_POLY:def 6;

 hence thesis by PRE_POLY:def 7;

 end;

 theorem :: BAGORD_2:47



 Th31: q is ordered & q = ( <*a*> ^ p) & (a . x) > 0 implies (a . x) = (b . x)

 proof

 assume

 Z0: q is ordered;

 assume

 Z1: q = ( <*a*> ^ p);

 assume

 Z2: (a . x) > 0 ;

 a in {a} = ( rng <*a*>) by TARSKI:def 1, FINSEQ_1: 39;

 then a in (( rng <*a*>) \/ ( rng p)) = ( rng q) by Z1, XBOOLE_0:def 3, FINSEQ_1: 31;

 hence thesis by Z0, Z2;

 end;

 theorem :: BAGORD_2:48



 Th32: q is ordered & q = ( <*a*> ^ p) & (a . x) > 0 & (a . y) > 0 & x <> y implies x ## y

 proof

 assume

 Z0: q is ordered;

 assume

 Z1: q = ( <*a*> ^ p);

 assume

 Z2: (a . x) > 0 & (a . y) > 0 ;

 a in {a} = ( rng <*a*>) by TARSKI:def 1, FINSEQ_1: 39;

 then a in (( rng <*a*>) \/ ( rng p)) = ( rng q) by Z1, XBOOLE_0:def 3, FINSEQ_1: 31;

 hence thesis by Z0, Z2;

 end;

 theorem :: BAGORD_2:49



 Th32A: q is ordered & q = ( <*a*> ^ p) implies a <> ( EmptyBag the carrier of R)

 proof

 assume

 Z0: q is ordered;

 assume

 Z1: q = ( <*a*> ^ p);

 a in {a} = ( rng <*a*>) by TARSKI:def 1, FINSEQ_1: 39;

 then a in (( rng <*a*>) \/ ( rng p)) = ( rng q) by Z1, XBOOLE_0:def 3, FINSEQ_1: 31;

 hence thesis by Z0;

 end;

 theorem :: BAGORD_2:50

 for c be bag of the carrier of R, r be ( Bags the carrier of R) -valued FinSequence st q is ordered & q = ( <*a, c*> ^ r) & (c . y) > 0 holds ex x st (a . x) > 0 & y <= x

 proof

 let c be bag of the carrier of R;

 let r be ( Bags the carrier of R) -valued FinSequence;

 assume

 Z0: q is ordered;

 assume

 Z1: q = ( <*a, c*> ^ r);

 assume

 Z2: (c . y) > 0 ;

 ( len <*a, c*>) = 2 by FINSEQ_1: 44;

 then

 A1: 1 in ( dom <*a, c*>) & 2 in ( dom <*a, c*>) & ( dom <*a, c*>) c= ( dom q) by Z1, FINSEQ_1: 26, FINSEQ_3: 25;

 (q /. 1) = (q . 1) = ( <*a, c*> . 1) = a & (q /. (1 + 1)) = (q . 2) = ( <*a, c*> . 2) = c by Z1, A1, PARTFUN1:def 6, FINSEQ_1:def 7, FINSEQ_1: 44;

 hence thesis by Z0, Z2, A1;

 end;

 theorem :: BAGORD_2:51

 x in I & (for y st y in I & y <> x holds x ## y) implies x is_maximal_in I

 proof

 assume

 Z0: x in I;

 assume

 Z1: for y st y in I & y <> x holds x ## y;

 not ex y st y in I & x < y

 proof

 let y;

 assume y in I & x <= y & x <> y;

 then x ## y & x <= y by Z1;

 hence contradiction;

 end;

 hence x is_maximal_in I by Z0, WAYBEL_4: 55;

 end;

 theorem :: BAGORD_2:52



 Th36: q is ordered & q = ( <*a*> ^ p) & c in ( rng p) & (c . x) > 0 implies ex y st (a . y) > 0 & x <= y

 proof

 assume

 Z0: q is ordered;

 assume

 Z1: q = ( <*a*> ^ p);

 assume c in ( rng p);

 then

 consider i be object such that

 A1: i in ( dom p) & c = (p . i) by FUNCT_1:def 3;

 reconsider i as Nat by A1;



 A2: 1 <= i & (p . i) = (p /. i) by A1, FINSEQ_3: 25, PARTFUN1:def 6;

 defpred P[ Nat] means $1 in ( dom p) implies for x st ((p /. $1) . x) > 0 holds ex y st (a . y) > 0 & x <= y;



 A5: ( len <*a*>) = 1 & ( dom <*a*>) c= ( dom q) by Z1, FINSEQ_1: 26, FINSEQ_1: 40;



 A3: P[1]

 proof

 assume

 A4: 1 in ( dom p);

 then

 A6: (1 + 1) in ( dom q) by Z1, A5, FINSEQ_1: 28;



 B0: 1 in ( dom <*a*>) by A5, FINSEQ_3: 25;

 then 1 in ( dom q) & (q . 1) = ( <*a*> . 1) = a by Z1, A5, FINSEQ_1:def 7, FINSEQ_1: 40;

 then (q /. 1) = a & (q /. 2) = (q . 2) = (p . 1) = (p /. 1) by Z1, A4, A5, A6, FINSEQ_1:def 7, PARTFUN1:def 6;

 hence thesis by Z0, A6, A5, B0;

 end;



 A8: for i be Nat st i >= 1 & P[i] holds P[(i + 1)]

 proof

 let i be Nat;

 assume

 B1: i >= 1 & P[i] & (i + 1) in ( dom p);

 then i < (i + 1) <= ( len p) by NAT_1: 13, FINSEQ_3: 25;

 then

 BB: i <= ( len p) by XXREAL_0: 2;

 then

 B3: i in ( dom p) by B1, FINSEQ_3: 25;



 B4: (1 + i) in ( dom q) & ((1 + i) + 1) in ( dom q) by Z1, A5, B1, BB, FINSEQ_3: 25, FINSEQ_1: 28;



 B5: (q /. (1 + i)) = (q . (1 + i)) = (p . i) = (p /. i) & (q /. ((1 + i) + 1)) = (q . ((1 + i) + 1)) = (p . (i + 1)) = (p /. (i + 1)) by Z1, A5, B1, B3, FINSEQ_1: 28, FINSEQ_1:def 7, PARTFUN1:def 6;

 let x;

 assume ((p /. (i + 1)) . x) > 0 ;

 then

 consider y such that

 B6: ((p /. i) . y) > 0 & x <= y by Z0, B4, B5;

 consider z such that

 B7: (a . z) > 0 & y <= z by BB, B1, FINSEQ_3: 25, B6;

 take z;

 thus (a . z) > 0 & x <= z by B6, B7, ORDERS_2: 3;

 end;

 for i be Nat st i >= 1 holds P[i] from NAT_1:sch 8( A3, A8);

 hence thesis by A1, A2;

 end;

 theorem :: BAGORD_2:53



 Th34: q is ordered & q = ( <*a*> ^ p) implies (x is_maximal_in ( support b) iff (a . x) > 0 )

 proof

 assume

 Z0: q is ordered;

 assume

 Z1: q = ( <*a*> ^ p);

 ( rng p) c= ( Bags the carrier of R) by RELAT_1:def 19;

 then

 reconsider p as FinSequence of ( Bags the carrier of R) by FINSEQ_1:def 4;

 set I = the carrier of R;

 hereby

 assume x is_maximal_in ( support b);

 then

 A7: x in ( support b) & not ex y st y in ( support b) & x < y by WAYBEL_4: 55;

 then x in ( support ( Sum q)) by PART;

 then

 consider d be bag of the carrier of R such that

 A8: d in ( rng q) & x in ( support d) by Th27;

 consider i be object such that

 A9: i in ( dom q) & d = (q . i) by A8, FUNCT_1:def 3;

 reconsider i as Nat by A9;

 1 <= i by A9, FINSEQ_3: 25;

 per cases by XXREAL_0: 1;

 suppose i = 1;

 then d = a by Z1, A9, FINSEQ_1: 41;

 then (a . x) <> 0 by A8, PRE_POLY:def 7;

 hence (a . x) > 0 ;

 end;

 suppose i > 1;

 then i >= (1 + 1) by NAT_1: 13;

 then

 consider k be Nat such that

 A10: i = ((1 + 1) + k) by NAT_1: 10;

 1 <= (1 + k) <= ((1 + k) + 1) = i <= ( len q) by A9, A10, NAT_1: 11, FINSEQ_3: 25;

 then 1 <= (1 + k) <= ( len q) by XXREAL_0: 2;

 then

 A11: (1 + k) in ( dom q) by FINSEQ_3: 25;

 then

 A12: (q /. i) = (q . i) & (q /. (1 + k)) = (q . (1 + k)) by A9, PARTFUN1:def 6;

 (d . x) <> 0 by A8, PRE_POLY:def 7;

 then (d . x) > 0 & i = ((1 + k) + 1) by A10;

 then

 consider y such that

 A13: ((q /. (1 + k)) . y) > 0 & x <= y by Z0, A9, A11, A12;

 (q . (1 + k)) in ( rng q) by A11, FUNCT_1:def 3;

 then y in ( support (q /. (1 + k))) c= ( support ( Sum q)) = ( support b) by A13, A12, Th26, PART, BAGORDER: 21, PRE_POLY:def 7;

 hence (a . x) > 0 by A7, A13, Lem2;

 end;

 end;

 assume

 B0: (a . x) > 0 ;

 then

 B1: x in ( support a) by PRE_POLY:def 7;

 a in {a} = ( rng <*a*>) c= ( rng q) by Z1, TARSKI:def 1, FINSEQ_1: 39, FINSEQ_1: 29;

 then

 B4: a divides ( Sum q) = b by Th26, PART;

 then

 AA: ( support a) c= ( support b) by BAGORDER: 21;

 not ex y st y in ( support b) & x < y

 proof

 let y;

 assume

 B3: y in ( support b) & x <= y & x <> y;

 per cases ;

 suppose (a . y) > 0 ;

 then x ## y by Z0, Z1, B0, B3, Th32;

 hence contradiction by B3;

 end;

 suppose

 B5: (a . y) = 0 ;

 consider d be bag of the carrier of R such that

 B6: d in ( rng q) & y in ( support d) by B4, B3, Th27;



 B7: (d . y) <> 0 by B6, PRE_POLY:def 7;

 then not d in {a} & {a} = ( rng <*a*>) & ( rng q) = (( rng <*a*>) \/ ( rng p)) by Z1, B5, TARSKI:def 1, FINSEQ_1: 31, FINSEQ_1: 39;

 then (d . y) > 0 & d in ( rng p) by B6, B7, XBOOLE_0:def 3;

 then

 consider z such that

 B8: (a . z) > 0 & y <= z by Z0, Z1, Th36;

 x <= z & x ## z by Z0, Z1, B0, B3, B8, ORDERS_2: 3, Th32;

 hence contradiction;

 end;

 end;

 hence x is_maximal_in ( support b) by B1, AA, WAYBEL_4: 55;

 end;

 theorem :: BAGORD_2:54



 Th40: q is ordered & q = ( <*a*> ^ p) implies a = (b | { x : x is_maximal_in ( support b) })

 proof

 assume

 Z0: q is ordered;

 assume

 Z1: q = ( <*a*> ^ p);

 let y;

 set J = { x : x is_maximal_in ( support b) };

 per cases ;

 suppose

 A0: y in J;

 then

 consider x such that

 A1: y = x & x is_maximal_in ( support b);

 (a . y) > 0 by Z0, Z1, A1, Th34;



 hence (a . y) = (b . y) by Z0, Z1, Th31

 .= ((b | J) . y) by A0, BAR;

 end;

 suppose

 A2: not y in J;

 then not y is_maximal_in ( support b);

 then (a . y) <= 0 by Z0, Z1, Th34;



 hence (a . y) = 0

 .= ((b | J) . y) by A2, BAR;

 end;

 end;

 theorem :: BAGORD_2:55



 Lem10: for p be ( Bags I) -valued FinSequence st ( Sum p) = ( EmptyBag I) & for a be bag of I st a in ( rng p) holds a <> ( EmptyBag I) holds p = {}

 proof

 let p be ( Bags I) -valued FinSequence;

 assume

 Z0: ( Sum p) = ( EmptyBag I);

 assume

 Z1: for a be bag of I st a in ( rng p) holds a <> ( EmptyBag I);

 assume p <> {} ;

 then

 consider a be object such that

 A1: a in ( rng p) by XBOOLE_0: 7;

 ( rng p) c= ( Bags I) by RELAT_1:def 19;

 then

 reconsider a as Element of ( Bags I) by A1;

 consider x be object such that

 A2: x in I & (a . x) <> (( EmptyBag I) . x) by A1, Z1, PBOOLE:def 10;



 A4: (( EmptyBag I) . x) = 0 by A2, FUNCOP_1: 7;

 then

 A3: (a . x) > 0 by A2;

 thus thesis by A4, A3, Z0, A1, Th26, PRE_POLY:def 11;

 end;

 theorem :: BAGORD_2:56



 Lem11: for a,b be bag of I st a <> ( EmptyBag I) holds (a + b) <> ( EmptyBag I)

 proof

 let a,b be bag of I;

 given i be object such that

 A1: i in I & (a . i) <> (( EmptyBag I) . i);

 take i;

 thus i in I by A1;

 (( EmptyBag I) . i) = 0 by A1, FUNCOP_1: 7;

 then ((a . i) + (b . i)) <> (( EmptyBag I) . i) by A1;

 hence thesis by PRE_POLY:def 5;

 end;

 theorem :: BAGORD_2:57

 for p,q be partition of b st p is ordered & q is ordered holds p = q

 proof

 let p,q be partition of b;

 defpred P[ Nat] means for b, q st ( len q) = $1 & q is ordered holds for p be partition of b st p is ordered holds q = p;



 A1: P[ 0 ]

 proof

 let b, q;

 assume ( len q) = 0 & q is ordered;

 then

 A3: b = ( Sum q) & ( Sum ( <*> ( Bags the carrier of R))) = ( EmptyBag the carrier of R) & q = {} by PART, Th21;

 let p be partition of b;

 assume

 A4: p is ordered;

 ( Sum p) = b by PART;

 hence q = p by A3, A4, Lem10;

 end;



 A5: for i be Nat st P[i] holds P[(i + 1)]

 proof

 let i be Nat;

 assume

 A6: P[i];

 let b, q;

 assume

 A7: ( len q) = (i + 1) & q is ordered;

 then q <> {} & q is FinSequence of ( Bags the carrier of R) by RELAT_1:def 19, FINSEQ_1:def 4;

 then

 consider w be FinSequence of ( Bags the carrier of R), n be Element of ( Bags the carrier of R) such that

 A8: q = ( <*n*> ^ w) by FINSEQ_2: 130;

 reconsider w as partition of (b -' n) by A8, Th28;



 A9: b = ( Sum q) = (n + ( Sum w)) <> ( EmptyBag the carrier of R) by A8, A7, Th32A, Th25, Lem11, PART;

 let p be partition of b;

 assume

 A10: p is ordered;

 ( Sum p) = b & ( rng p) c= ( Bags the carrier of R) by PART, RELAT_1:def 19;

 then p <> ( <*> ( Bags the carrier of R)) & p is FinSequence of ( Bags the carrier of R) by A9, Th21, FINSEQ_1:def 4;

 then

 consider u be FinSequence of ( Bags the carrier of R), m be Element of ( Bags the carrier of R) such that

 A11: p = ( <*m*> ^ u) by FINSEQ_2: 130;

 reconsider u as partition of (b -' m) by A11, Th28;

 u = u & w = w;

 then

 A12: m = (b | { x : x is_maximal_in ( support b) }) = n by A10, A11, A7, A8, Th40;



 A13: w is ordered & u is ordered by A10, A11, A7, A8, Th30;

 ( len q) = (( len <*n*>) + ( len w)) = (1 + ( len w)) by A8, FINSEQ_1: 22, FINSEQ_1: 40;

 hence thesis by A6, A7, A8, A11, A12, A13;

 end;

 for i be Nat holds P[i] from NAT_1:sch 2( A1, A5);

 then P[( len p)];

 hence thesis;

 end;

 definition

 let I;

 let a,b be bag of I;

 :: original: [

 redefine

 func [a,b] -> Element of [:( Bags I), ( Bags I):] ;

 coherence

 proof

 a in ( Bags I) & b in ( Bags I) by PRE_POLY:def 12;

 hence thesis by ZFMISC_1: 87;

 end;

 end

 theorem :: BAGORD_2:58



 Th42: a <> ( EmptyBag the carrier of R) implies { x : x is_maximal_in ( support a) } <> {}

 proof

 set I = the carrier of R;

 given x such that

 A1: (a . x) <> (( EmptyBag I) . x);

 (( EmptyBag I) . x) = 0 by FUNCOP_1: 7;

 then x in ( support a) by A1, PRE_POLY:def 7;

 then

 consider x such that

 A2: x is_maximal_in ( support a) by Th12;

 x in { y : y is_maximal_in ( support a) } by A2;

 hence thesis;

 end;

 definition

 let R, b;

 :: BAGORD_2:def12

 func OrderedPartition b -> ( Bags the carrier of R) -valued FinSequence means

 : OP: ex F,G be Function of NAT , ( Bags the carrier of R) st (F . 0 ) = b & (G . 0 ) = ( EmptyBag the carrier of R) & (for i be Nat holds (G . (i + 1)) = ((F . i) | { x : x is_maximal_in ( support (F . i)) }) & (F . (i + 1)) = ((F . i) -' (G . (i + 1)))) & ex i be Nat st (F . i) = ( EmptyBag the carrier of R) & it = (G | ( Seg i)) & for j be Nat st j ( EmptyBag the carrier of R);

 existence

 proof

 set I = the carrier of R;

 deffunc S( bag of I) = { x : x is_maximal_in ( support $1) };

 deffunc h( Nat, Element of [:( Bags I), ( Bags I):]) = [(($2 `1 ) -' (($2 `1 ) | S(`1))), (($2 `1 ) | S(`1))];

 consider f be Function of NAT , [:( Bags I), ( Bags I):] such that

 A1: (f . 0 ) = [b, ( EmptyBag I)] & for i be Nat holds (f . (i + 1)) = h(i,.) from NAT_1:sch 12;

 defpred P[ Nat] means ex i be Nat st ( card ( support ((f . i) `1 ))) = $1;

 defpred Q[ Nat] means ( card ( support ((f . $1) `1 ))) = 0 ;



 A2: ex k be Nat st P[k]

 proof

 take k = ( card ( support ((f . 0 ) `1 )));

 take i = 0 ;

 thus thesis;

 end;



 A3: for k be Nat st k <> 0 & P[k] holds ex n be Nat st n < k & P[n]

 proof

 let k be Nat;

 assume

 Z0: k <> 0 ;

 given i be Nat such that

 Z1: ( card ( support ((f . i) `1 ))) = k;

 ((f . i) `1 ) <> ( EmptyBag I) by Z0, Z1;

 then

 B1: S(`1) <> {} by Th42;

 (f . (i + 1)) = h(i,.) by A1;

 then

 B2: ( support ((f . (i + 1)) `1 )) = (( support ((f . i) `1 )) \ S(`1)) by Th27A;

 S(`1) c= ( support ((f . i) `1 ))

 proof

 let x be object;

 assume x in S(`1);

 then ex y st x = y & y is_maximal_in ( support ((f . i) `1 ));

 hence thesis by WAYBEL_4: 55;

 end;

 then

 reconsider S = S(`1) as finite Subset of ( support ((f . i) `1 ));

 take n = ( card ( support ((f . (i + 1)) `1 )));

 ( card S) <> 0 by B1;

 then n = (k - ( card S)) & ( card S) > 0 by Z1, B2, CARD_2: 44;

 hence n < k by XREAL_1: 44;

 thus P[n];

 end;

 P[ 0 ] from NAT_1:sch 7( A2, A3);

 then

 A4: ex i be Nat st Q[i];

 consider i be Nat such that

 A5: Q[i] & for n be Nat st Q[n] holds i <= n from NAT_1:sch 5( A4);

 ( Seg i) c= NAT = ( dom ( pr2 f)) by FUNCT_2:def 1;

 then ( dom (( pr2 f) | ( Seg i))) = ( Seg i) by RELAT_1: 62;

 then

 reconsider p = (( pr2 f) | ( Seg i)) as ( Bags the carrier of R) -valued FinSequence by FINSEQ_1:def 2;

 take p;

 take F = ( pr1 f);

 take G = ( pr2 f);



 thus (F . 0 ) = ((f . 0 ) `1 ) by FUNCT_2:def 5

 .= b by A1;



 thus (G . 0 ) = ((f . 0 ) `2 ) by FUNCT_2:def 6

 .= ( EmptyBag I) by A1;

 hereby

 let i be Nat;

 reconsider j = i as Element of NAT by ORDINAL1:def 12;



 A6: (G . (i + 1)) = ((f . (i + 1)) `2 ) by FUNCT_2:def 6

 .= ( h(i,.) `2 ) by A1

 .= (((f . j) `1 ) | S(`1));

 ((f . j) `1 ) = (F . i) by FUNCT_2:def 5;

 hence (G . (i + 1)) = ((F . i) | S(.)) by A6;



 thus (F . (i + 1)) = ((f . (i + 1)) `1 ) by FUNCT_2:def 5

 .= ( h(i,.) `1 ) by A1

 .= (((f . j) `1 ) -' (G . (i + 1))) by A6

 .= ((F . i) -' (G . (i + 1))) by FUNCT_2:def 5;

 end;

 take i;

 reconsider j = i as Element of NAT by ORDINAL1:def 12;

 ( support ((f . i) `1 )) = {} by A5;

 then ((f . j) `1 ) = ( EmptyBag I) by PRE_POLY: 81;

 hence (F . i) = ( EmptyBag I) by FUNCT_2:def 5;

 thus p = (G | ( Seg i));

 let k be Nat;

 reconsider j = k as Element of NAT by ORDINAL1:def 12;

 assume k < i;

 then not Q[k] by A5;

 then ((f . j) `1 ) <> ( EmptyBag I);

 hence (F . k) <> ( EmptyBag I) by FUNCT_2:def 5;

 end;

 uniqueness

 proof

 let p1,p2 be ( Bags the carrier of R) -valued FinSequence;

 given F1,G1 be Function of NAT , ( Bags the carrier of R) such that

 A1: (F1 . 0 ) = b & (G1 . 0 ) = ( EmptyBag the carrier of R) & (for i be Nat holds (G1 . (i + 1)) = ((F1 . i) | { x : x is_maximal_in ( support (F1 . i)) }) & (F1 . (i + 1)) = ((F1 . i) -' (G1 . (i + 1)))) & ex i be Nat st (F1 . i) = ( EmptyBag the carrier of R) & p1 = (G1 | ( Seg i)) & for j be Nat st j ( EmptyBag the carrier of R);

 given F2,G2 be Function of NAT , ( Bags the carrier of R) such that

 A2: (F2 . 0 ) = b & (G2 . 0 ) = ( EmptyBag the carrier of R) & (for i be Nat holds (G2 . (i + 1)) = ((F2 . i) | { x : x is_maximal_in ( support (F2 . i)) }) & (F2 . (i + 1)) = ((F2 . i) -' (G2 . (i + 1)))) & ex i be Nat st (F2 . i) = ( EmptyBag the carrier of R) & p2 = (G2 | ( Seg i)) & for j be Nat st j ( EmptyBag the carrier of R);

 defpred P[ Nat] means (G1 . $1) = (G2 . $1) & (F1 . $1) = (F2 . $1);



 A3: P[ 0 ] by A1, A2;



 A4: for i be Nat st P[i] holds P[(i + 1)]

 proof

 let i be Nat;

 assume

 A5: P[i];



 hence (G1 . (i + 1)) = ((F2 . i) | { x : x is_maximal_in ( support (F2 . i)) }) by A1

 .= (G2 . (i + 1)) by A2;



 hence (F1 . (i + 1)) = ((F2 . i) -' (G2 . (i + 1))) by A1, A5

 .= (F2 . (i + 1)) by A2;

 end;



 A6: for i be Nat holds P[i] from NAT_1:sch 2( A3, A4);



 A7: F1 = F2

 proof

 let i be Element of NAT ;

 thus (F1 . i) = (F2 . i) by A6;

 end;



 A8: G1 = G2

 proof

 let i be Element of NAT ;

 thus (G1 . i) = (G2 . i) by A6;

 end;

 consider i1 be Nat such that

 A9: (F1 . i1) = ( EmptyBag the carrier of R) & p1 = (G1 | ( Seg i1)) & for j be Nat st j < i1 holds (F1 . j) <> ( EmptyBag the carrier of R) by A1;

 consider i2 be Nat such that

 AA: (F1 . i2) = ( EmptyBag the carrier of R) & p2 = (G1 | ( Seg i2)) & for j be Nat st j < i2 holds (F1 . j) <> ( EmptyBag the carrier of R) by A2, A7, A8;

 i1 <= i2 <= i1 by A9, AA;

 hence p1 = p2 by A9, AA, XXREAL_0: 1;

 end;

 end

 definition

 let R, b;

 :: original: OrderedPartition

 redefine

 func OrderedPartition b -> partition of b ;

 coherence

 proof

 set p = ( OrderedPartition b);

 consider F,G be Function of NAT , ( Bags the carrier of R) such that

 A1: (F . 0 ) = b & (G . 0 ) = ( EmptyBag the carrier of R) & (for i be Nat holds (G . (i + 1)) = ((F . i) | { x : x is_maximal_in ( support (F . i)) }) & (F . (i + 1)) = ((F . i) -' (G . (i + 1)))) & ex i be Nat st (F . i) = ( EmptyBag the carrier of R) & p = (G | ( Seg i)) & for j be Nat st j ( EmptyBag the carrier of R) by OP;

 consider i be Nat such that

 A2: (F . i) = ( EmptyBag the carrier of R) & p = (G | ( Seg i)) & for j be Nat st j ( EmptyBag the carrier of R) by A1;

 defpred P[ Nat] means $1 <= i implies b = ((F . $1) + ( Sum (p | $1)));

 set I = the carrier of R;



 A3: P[ 0 ]

 proof

 (p | 0 ) = ( <*> ( Bags I));

 then ( Sum (p | 0 )) = ( EmptyBag I) by Th21;

 hence 0 <= i implies b = ((F . 0 ) + ( Sum (p | 0 ))) by A1, PRE_POLY: 53;

 end;

 ( dom G) = NAT by FUNCT_2:def 1;

 then ( dom p) = ( Seg i) & i in NAT by A2, RELAT_1: 62, ORDINAL1:def 12;

 then

 A5: ( len p) = i by FINSEQ_1:def 3;



 A4: for j be Nat st P[j] holds P[(j + 1)]

 proof

 let j be Nat;

 assume

 B1: P[j] & (j + 1) <= i;

 ( rng p) c= ( Bags I) by RELAT_1:def 19;

 then

 reconsider q = p as FinSequence of ( Bags I) by FINSEQ_1:def 4;



 B2: (q | (j + 1)) = ((q | j) ^ <*(q /. (j + 1))*>) by B1, A5, FINSEQ_5: 82;

 (j + 1) in ( dom p) by A5, B1, NAT_1: 11, FINSEQ_3: 25;

 then

 B4: (q /. (j + 1)) = (p . (j + 1)) = (G . (j + 1)) by A2, PARTFUN1:def 6, FUNCT_1: 47;

 (G . (j + 1)) = ((F . j) | { x : x is_maximal_in ( support (F . j)) }) by A1;

 then (F . (j + 1)) = ((F . j) -' (G . (j + 1))) & (G . (j + 1)) divides (F . j) by A1, Th43;

 then ((F . (j + 1)) + (G . (j + 1))) = (F . j) by PRE_POLY: 47;



 hence b = ((F . (j + 1)) + ((G . (j + 1)) + ( Sum (p | j)))) by B1, NAT_1: 13, RFUNCT_1: 8

 .= ((F . (j + 1)) + ( Sum (p | (j + 1)))) by B2, B4, Th22;

 end;

 for j be Nat holds P[j] from NAT_1:sch 2( A3, A4);

 then P[( len p)] & (p | ( len p)) = p by FINSEQ_1: 58;

 hence b = ( Sum p) by A2, A5, PRE_POLY: 53;

 end;

 end

 registration

 let R, b;

 cluster ( OrderedPartition b) -> ordered;

 coherence

 proof

 let p be partition of b such that

 A0: p = ( OrderedPartition b);

 consider F,G be Function of NAT , ( Bags the carrier of R) such that

 A1: (F . 0 ) = b & (G . 0 ) = ( EmptyBag the carrier of R) & (for i be Nat holds (G . (i + 1)) = ((F . i) | { x : x is_maximal_in ( support (F . i)) }) & (F . (i + 1)) = ((F . i) -' (G . (i + 1)))) & ex i be Nat st (F . i) = ( EmptyBag the carrier of R) & p = (G | ( Seg i)) & for j be Nat st j ( EmptyBag the carrier of R) by OP, A0;

 consider i be Nat such that

 A2: (F . i) = ( EmptyBag the carrier of R) & p = (G | ( Seg i)) & for j be Nat st j ( EmptyBag the carrier of R) by A1;

 set I = the carrier of R;

 ( dom G) = NAT by FUNCT_2:def 1;

 then ( dom p) = ( Seg i) & i in NAT by A2, RELAT_1: 62, ORDINAL1:def 12;

 then

 A3: ( len p) = i by FINSEQ_1:def 3;

 defpred P[ Nat] means for x st ((F . $1) . x) > 0 holds ((F . $1) . x) = (b . x);



 A4: P[ 0 ] by A1;



 A5: for j be Nat st P[j] holds P[(j + 1)]

 proof

 let j be Nat;

 assume

 A6: P[j];

 let x;

 assume

 A7: ((F . (j + 1)) . x) > 0 ;

 set S = { y : y is_maximal_in ( support (F . j)) };

 (F . (j + 1)) = ((F . j) -' (G . (j + 1))) & (G . (j + 1)) = ((F . j) | S) by A1;

 then

 A8: ((F . (j + 1)) . x) = (((F . j) . x) -' (((F . j) | S) . x)) by PRE_POLY:def 6;

 per cases ;

 suppose x in S;

 then (((F . j) | S) . x) = ((F . j) . x) by BAR;

 hence thesis by A7, A8, XREAL_1: 232;

 end;

 suppose not x in S;

 then (((F . j) | S) . x) = 0 by BAR;

 then ((F . (j + 1)) . x) = ((F . j) . x) by A8, NAT_D: 40;

 hence thesis by A6, A7;

 end;

 end;



 A9: for j be Nat holds P[j] from NAT_1:sch 2( A4, A5);

 hereby

 let a;

 assume a in ( rng p);

 then

 consider j be object such that

 B1: j in ( dom p) & a = (p . j) by FUNCT_1:def 3;

 reconsider j as Nat by B1;

 consider k be Nat such that

 B2: j = (1 + k) by B1, FINSEQ_3: 25, NAT_1: 10;

 set S = { x : x is_maximal_in ( support (F . k)) };



 B3: a = (G . j) = ((F . k) | S) by A1, B2, B1, FUNCT_1: 47;

 let x;

 assume

 B4: (a . x) > 0 ;

 then x in S by B3, BAR;

 then (a . x) = ((F . k) . x) by B3, BAR;

 hence (a . x) = (b . x) by A9, B4;

 end;

 hereby

 let a;

 assume a in ( rng p);

 then

 consider j be object such that

 B1: j in ( dom p) & a = (p . j) by FUNCT_1:def 3;

 reconsider j as Nat by B1;

 consider k be Nat such that

 B2: j = (1 + k) by B1, FINSEQ_3: 25, NAT_1: 10;



 B3: a = (G . j) = ((F . k) | { x : x is_maximal_in ( support (F . k)) }) by A1, B2, B1, FUNCT_1: 47;

 { x : x is_maximal_in ( support (F . k)) } c= ( support (F . k))

 proof

 let z be object;

 assume z in { x : x is_maximal_in ( support (F . k)) };

 then ex x st z = x & x is_maximal_in ( support (F . k));

 hence thesis by WAYBEL_4: 55;

 end;

 then (( support (F . k)) /\ { x : x is_maximal_in ( support (F . k)) }) = { y : y is_maximal_in ( support (F . k)) } by XBOOLE_1: 28;

 then

 B4: ( support a) = { x : x is_maximal_in ( support (F . k)) } by B3, Th44;

 let x, y;

 assume

 B5: (a . x) > 0 & (a . y) > 0 & x <> y;

 then x in ( support a) by PRE_POLY:def 7;

 then

 consider z such that

 B6: x = z & z is_maximal_in ( support (F . k)) by B4;

 y in ( support a) by B5, PRE_POLY:def 7;

 then

 consider u be Element of R such that

 B7: y = u & u is_maximal_in ( support (F . k)) by B4;

 x in ( support (F . k)) & y in ( support (F . k)) by B6, B7, WAYBEL_4: 55;

 then not x < y & not y < x by B6, B7, WAYBEL_4: 55;

 hence x ## y by Lem2;

 end;

 hereby

 let a;

 assume a in ( rng p);

 then

 consider j be object such that

 B1: j in ( dom p) & a = (p . j) by FUNCT_1:def 3;

 reconsider j as Nat by B1;

 consider k be Nat such that

 B2: j = (1 + k) by B1, FINSEQ_3: 25, NAT_1: 10;



 B3: a = (G . j) = ((F . k) | { x : x is_maximal_in ( support (F . k)) }) by A1, B2, B1, FUNCT_1: 47;

 k < j <= i by A3, B2, B1, NAT_1: 13, FINSEQ_3: 25;

 then k {} by A2, Th42;

 { x : x is_maximal_in ( support (F . k)) } c= ( support (F . k))

 proof

 let z be object;

 assume z in { x : x is_maximal_in ( support (F . k)) };

 then ex x st z = x & x is_maximal_in ( support (F . k));

 hence thesis by WAYBEL_4: 55;

 end;

 then (( support (F . k)) /\ { x : x is_maximal_in ( support (F . k)) }) = { y : y is_maximal_in ( support (F . k)) } by XBOOLE_1: 28;

 then ( support a) = { x : x is_maximal_in ( support (F . k)) } by B3, Th44;

 hence a <> ( EmptyBag the carrier of R) by B4;

 end;

 let j be Nat;

 assume

 C1: j in ( dom p) & (j + 1) in ( dom p);

 then

 consider k be Nat such that

 B2: j = (1 + k) by NAT_1: 10, FINSEQ_3: 25;

 let x;

 assume

 C2: ((p /. (j + 1)) . x) > 0 ;

 set S = { y : y is_maximal_in ( support (F . j)) };

 set T = { y : y is_maximal_in ( support (F . k)) };



 C4: (p /. (j + 1)) = (p . (j + 1)) = (G . (j + 1)) = ((F . j) | S) & (p /. j) = (p . j) = (G . j) = ((F . k) | T) & (F . j) = ((F . k) -' (G . j)) by C1, B2, A1, FUNCT_1: 47, PARTFUN1:def 6;

 then x in S by C2, BAR;

 then

 consider y such that

 C5: x = y & y is_maximal_in ( support (F . j));



 C6: x in ( support (F . j)) c= ( support (F . k)) by C4, C5, WAYBEL_4: 55, PRE_POLY: 39;

 T c= ( support (F . k))

 proof

 let u be object;

 assume u in T;

 then ex z st u = z & z is_maximal_in ( support (F . k));

 hence thesis by WAYBEL_4: 55;

 end;

 then (( support (F . k)) /\ T) = T by XBOOLE_1: 28;

 then

 D2: ( support (p /. j)) = T by C4, Th44;

 ( support (F . j)) = (( support (F . k)) \ T) by C4, Th27A;

 then not x in T by C6, XBOOLE_0:def 5;

 then not x is_maximal_in ( support (F . k));

 then

 consider z such that

 C7: z in ( support (F . k)) & x < z by C6, WAYBEL_4: 55;

 take z;

 not z in ( support (F . j)) & ( support (F . j)) = (( support (F . k)) \ T) by C4, C5, C7, Th27A, WAYBEL_4: 55;

 then z in T by C7, XBOOLE_0:def 5;

 then ((p /. j) . z) <> 0 by D2, PRE_POLY:def 7;

 hence ((p /. j) . z) > 0 ;

 thus x <= z by C7, Lem2;

 end;

 end

 theorem :: BAGORD_2:59

 b = ( EmptyBag the carrier of R) iff ( OrderedPartition b) = {}

 proof

 set I = the carrier of R;

 set E = ( EmptyBag I);

 set p = ( OrderedPartition b);

 consider F,G be Function of NAT , ( Bags the carrier of R) such that

 A1: (F . 0 ) = b & (G . 0 ) = E & (for i be Nat holds (G . (i + 1)) = ((F . i) | { x : x is_maximal_in ( support (F . i)) }) & (F . (i + 1)) = ((F . i) -' (G . (i + 1)))) & ex i be Nat st (F . i) = E & p = (G | ( Seg i)) & for j be Nat st j E by OP;

 consider i be Nat such that

 A2: (F . i) = E & p = (G | ( Seg i)) & for j be Nat st j E by A1;

 hereby

 assume b = E;

 then i <= 0 by A1, A2;

 then i = 0 ;

 hence p = {} by A2;

 end;

 assume p = {} ;

 then p = ( <*> ( Bags I));

 then ( Sum p) = E by Th21;

 hence thesis by PART;

 end;

 definition

 let R;

 :: BAGORD_2:def13

 func PrecM R -> strict RelExtension of ( finite-MultiSet_over the carrier of R) means

 : PM: for m,n be Element of it holds m <= n iff m <> n & for x st (m . x) > 0 holds (m . x) < (n . x) or ex y st (n . y) > 0 & x <= y;

 existence

 proof

 set I = the carrier of R;

 set M = ( finite-MultiSet_over I);

 defpred R[ bag of I, bag of I] means $1 <> $2 & for x st ($1 . x) > 0 holds ($1 . x) < ($2 . x) or ex y st ($2 . y) > 0 & x <= y;

 consider N be strict RelExtension of M such that

 A1: for m,n be Element of N holds m <= n iff R[m, n] from RelEx;

 take N;

 thus thesis by A1;

 end;

 uniqueness

 proof

 let N1,N2 be strict RelExtension of ( finite-MultiSet_over the carrier of R) such that

 A1: for m,n be Element of N1 holds m <= n iff m <> n & for x st (m . x) > 0 holds (m . x) < (n . x) or ex y st (n . y) > 0 & x <= y and

 A2: for m,n be Element of N2 holds m <= n iff m <> n & for x st (m . x) > 0 holds (m . x) < (n . x) or ex y st (n . y) > 0 & x <= y;

 for m,n be Element of N1 holds for x,y be Element of N2 st m = x & n = y holds m <= n iff x <= y

 proof

 let m,n be Element of N1;

 let k,l be Element of N2;

 assume

 Z0: m = k;

 assume

 Z1: n = l;

 m <= n iff m <> n & for x st (m . x) > 0 holds (m . x) < (n . x) or ex y st (n . y) > 0 & x <= y by A1;

 hence thesis by A2, Z0, Z1;

 end;

 hence thesis by Th4;

 end;

 end

 registration

 let R;

 cluster ( PrecM R) -> asymmetric transitive;

 coherence

 proof

 set RR = the InternalRel of ( PrecM R);

 thus

 A0: ( PrecM R) is asymmetric

 proof

 let a,b be object;

 assume a in the carrier of ( PrecM R) & b in the carrier of ( PrecM R);

 then

 reconsider m = a, n = b as Element of ( PrecM R);

 assume [a, b] in RR & [b, a] in RR;

 then

 A0: m <= n & n <= m by ORDERS_2:def 5;

 then m <> n & (for x st (m . x) > 0 holds (m . x) < (n . x) or ex y st (n . y) > 0 & x <= y) & (for x st (n . x) > 0 holds (n . x) < (m . x) or ex y st (m . y) > 0 & x <= y) by PM;

 then

 consider x such that

 A2: (m . x) <> (n . x) by PBOOLE:def 21;

 set X = { y : (m . y) > 0 & x <= y };

 ex y st (m . y) > 0 & x <= y

 proof

 per cases by A2, XXREAL_0: 1;

 suppose (m . x) < (n . x);

 hence ex y st (m . y) > 0 & x <= y by A0, PM;

 end;

 suppose (n . x) < (m . x);

 then

 consider y such that

 A5: (n . y) > 0 & x <= y by A0, PM;

 per cases by A0, PM;

 suppose (n . y) <= (m . y);

 hence ex y st (m . y) > 0 & x <= y by A5;

 end;

 suppose ex z st (m . z) > 0 & y <= z;

 hence ex y st (m . y) > 0 & x <= y by A5, ORDERS_2: 3;

 end;

 end;

 end;

 then

 consider y such that

 A6: (m . y) > 0 & x <= y;



 A7: y in X by A6;

 X c= ( support m)

 proof

 let z be object;

 assume z in X;

 then ex y st z = y & (m . y) > 0 & x <= y;

 hence thesis by PRE_POLY:def 7;

 end;

 then

 consider y such that

 A8: y is_maximal_in X by A7, Th12;

 y in X by A8, WAYBEL_4: 55;

 then

 consider z such that

 A9: y = z & (m . z) > 0 & x <= z;

 per cases by A0, PM, A9;

 suppose (m . z) < (n . z);

 then

 consider u be Element of R such that

 A10: (m . u) > 0 & z <= u by A0, PM;

 x <= u by A9, A10, ORDERS_2: 3;

 then u in X & y 0 & z <= u;

 then

 consider u be Element of R such that

 A11: (n . u) > 0 & z <= u;

 per cases by A0, PM;

 suppose (n . u) <= (m . u);

 then (m . u) > 0 & x <= u by A9, A11, ORDERS_2: 3;

 then u in X & y 0 & u <= v;

 then

 consider v be Element of R such that

 A12: (m . v) > 0 & u <= v;



 A13: z <= v by A11, A12, ORDERS_2: 3;

 then x <= v by A9, ORDERS_2: 3;

 then v in X & y < v by A9, A12, A13, Lem2;

 hence contradiction by A8, WAYBEL_4: 55;

 end;

 end;

 end;

 thus ( PrecM R) is transitive

 proof

 let a,b,c be object;

 assume a in the carrier of ( PrecM R) & b in the carrier of ( PrecM R) & c in the carrier of ( PrecM R);

 assume

 A4: [a, b] in RR & [b, c] in RR;

 then

 reconsider a, b, c as Element of ( PrecM R) by ZFMISC_1: 87;



 A6: a <= b <= c by A4, ORDERS_2:def 5;

 A5:

 now

 let x;

 assume (a . x) > 0 ;

 per cases by A6, PM;

 suppose

 A4: (a . x) < (b . x);

 then (b . x) < (c . x) or ex y st (c . y) > 0 & x <= y by A6, PM;

 hence (a . x) < (c . x) or ex y st (c . y) > 0 & x <= y by A4, XXREAL_0: 2;

 end;

 suppose ex y st (b . y) > 0 & x <= y;

 then

 consider y such that

 B1: (b . y) > 0 & x <= y;

 per cases by A6, PM;

 suppose (b . y) <= (c . y);

 hence (a . x) < (c . x) or ex y st (c . y) > 0 & x <= y by B1;

 end;

 suppose ex z st (c . z) > 0 & y <= z;

 then

 consider z such that

 B2: (c . z) > 0 & y <= z;

 thus (a . x) < (c . x) or ex y st (c . y) > 0 & x <= y by B2, B1, ORDERS_2: 3;

 end;

 end;

 end;

 a <> c by A4, A0, PREFER_1: 22;

 then a <= c by A5, PM;

 hence thesis by ORDERS_2:def 5;

 end;

 end;

 end

 definition

 let I;

 let R be Relation of I, I;

 :: BAGORD_2:def14

 func LexOrder (I,R) -> Relation of (I * ) means

 : LO: for p,q be I -valued FinSequence holds [p, q] in it iff p c< q or ex k be Nat st k in ( dom p) & k in ( dom q) & [(p . k), (q . k)] in R & for n be Nat st 1 <= n < k holds (p . n) = (q . n);

 existence

 proof

 defpred R[ Element of (I * ), Element of (I * )] means $1 c< $2 or ex k be Nat st k in ( dom $1) & k in ( dom $2) & [($1 . k), ($2 . k)] in R & for n be Nat st 1 <= n < k holds ($1 . n) = ($2 . n);

 consider R be Relation of (I * ) such that

 A1: for b1,b2 be Element of (I * ) holds [b1, b2] in R iff R[b1, b2] from RELSET_1:sch 2;

 take R;

 let b1,b2 be I -valued FinSequence;

 ( rng b1) c= I & ( rng b2) c= I by RELAT_1:def 19;

 then b1 is FinSequence of I & b2 is FinSequence of I by FINSEQ_1:def 4;

 then b1 in (I * ) & b2 in (I * ) by FINSEQ_1:def 11;

 hence thesis by A1;

 end;

 uniqueness

 proof

 let R1,R2 be Relation of (I * ) such that

 A1: for p,q be I -valued FinSequence holds [p, q] in R1 iff p c< q or ex k be Nat st k in ( dom p) & k in ( dom q) & [(p . k), (q . k)] in R & for n be Nat st 1 <= n < k holds (p . n) = (q . n) and

 A2: for p,q be I -valued FinSequence holds [p, q] in R2 iff p c< q or ex k be Nat st k in ( dom p) & k in ( dom q) & [(p . k), (q . k)] in R & for n be Nat st 1 <= n < k holds (p . n) = (q . n);

 let p,q be Element of (I * );

 [p, q] in R1 iff p c< q or ex k be Nat st k in ( dom p) & k in ( dom q) & [(p . k), (q . k)] in R & for n be Nat st 1 <= n < k holds (p . n) = (q . n) by A1;

 hence thesis by A2;

 end;

 end

 registration

 let I;

 let R be transitive Relation of I;

 cluster ( LexOrder (I,R)) -> transitive;

 coherence

 proof

 set Q = ( LexOrder (I,R));

 let a,b,c be object;

 assume a in ( field Q) & b in ( field Q) & c in ( field Q);

 assume

 A1: [a, b] in Q & [b, c] in Q;

 then

 reconsider a, b, c as Element of (I * ) by ZFMISC_1: 87;

 per cases by A1, LO;

 suppose a c< b & b c< c;

 then a c< c by XBOOLE_1: 56;

 hence thesis by LO;

 end;

 suppose

 A2: a c< b & ex k be Nat st k in ( dom b) & k in ( dom c) & [(b . k), (c . k)] in R & for n be Nat st 1 <= n < k holds (b . n) = (c . n);

 then

 consider k be Nat such that

 A3: k in ( dom b) & k in ( dom c) & [(b . k), (c . k)] in R & for n be Nat st 1 <= n < k holds (b . n) = (c . n);

 per cases ;

 suppose

 A4: ( len a) < k;

 k <= ( len c) by A3, FINSEQ_3: 25;

 then

 A5: ( len a) < ( len c) by A4, XXREAL_0: 2;

 for n be Nat st n in ( dom a) holds (a . n) = (c . n)

 proof

 let n be Nat;

 assume

 A6: n in ( dom a);

 then n <= ( len a) by FINSEQ_3: 25;

 then 1 <= n < k by A4, A6, XXREAL_0: 2, FINSEQ_3: 25;

 then (b . n) = (c . n) by A3;

 hence thesis by A2, A6, Lem12;

 end;

 then a c< c by A5, Lem12;

 hence thesis by LO;

 end;

 suppose

 A7: ( len a) >= k;

 1 <= k by A3, FINSEQ_3: 25;

 then

 A8: k in ( dom a) by A7, FINSEQ_3: 25;

 then

 A9: [(a . k), (c . k)] in R by A2, A3, Lem12;

 for n be Nat st 1 <= n < k holds (a . n) = (c . n)

 proof

 let n be Nat;

 assume

 A10: 1 <= n < k;

 then n < ( len a) by A7, XXREAL_0: 2;

 then n in ( dom a) by A10, FINSEQ_3: 25;

 then (a . n) = (b . n) by A2, Lem12;

 hence thesis by A10, A3;

 end;

 hence thesis by A3, A8, A9, LO;

 end;

 end;

 suppose

 A12: b c< c & ex k be Nat st k in ( dom a) & k in ( dom b) & [(a . k), (b . k)] in R & for n be Nat st 1 <= n < k holds (a . n) = (b . n);

 then

 consider k be Nat such that

 A11: k in ( dom a) & k in ( dom b) & [(a . k), (b . k)] in R & for n be Nat st 1 <= n < k holds (a . n) = (b . n);

 ( dom b) c= ( dom c) by A12, XBOOLE_0:def 8, XTUPLE_0: 8;

 then

 A13: k in ( dom c) & [(a . k), (c . k)] in R by A12, A11, Lem12;

 for n be Nat st 1 <= n < k holds (a . n) = (c . n)

 proof

 let n be Nat;

 assume

 A14: 1 <= n < k;

 k <= ( len b) by A11, FINSEQ_3: 25;

 then n < ( len b) by A14, XXREAL_0: 2;

 then (b . n) = (c . n) by A12, Lem12, A14, FINSEQ_3: 25;

 hence thesis by A11, A14;

 end;

 hence thesis by A11, A13, LO;

 end;

 suppose

 A15: (ex k be Nat st k in ( dom a) & k in ( dom b) & [(a . k), (b . k)] in R & for n be Nat st 1 <= n < k holds (a . n) = (b . n)) & ex k be Nat st k in ( dom b) & k in ( dom c) & [(b . k), (c . k)] in R & for n be Nat st 1 <= n < k holds (b . n) = (c . n);

 then

 consider k1 be Nat such that

 A16: k1 in ( dom a) & k1 in ( dom b) & [(a . k1), (b . k1)] in R & for n be Nat st 1 <= n < k1 holds (a . n) = (b . n);

 consider k2 be Nat such that

 A17: k2 in ( dom b) & k2 in ( dom c) & [(b . k2), (c . k2)] in R & for n be Nat st 1 <= n < k2 holds (b . n) = (c . n) by A15;

 per cases by XXREAL_0: 1;

 suppose

 A18: k1 < k2;

 k2 <= ( len c) by A17, FINSEQ_3: 25;

 then 1 <= k1 < ( len c) by A16, A18, FINSEQ_3: 25, XXREAL_0: 2;

 then

 A19: k1 in ( dom c) & [(a . k1), (c . k1)] in R by A16, A17, A18, FINSEQ_3: 25;

 for n be Nat st 1 <= n < k1 holds (a . n) = (c . n)

 proof

 let n be Nat;

 assume 1 <= n < k1;

 then (a . n) = (b . n) & 1 <= n < k2 by A16, A18, XXREAL_0: 2;

 hence thesis by A17;

 end;

 hence thesis by A16, A19, LO;

 end;

 suppose

 A20: k1 = k2;

 then

 A21: [(a . k1), (c . k1)] in R by A16, A17, RELAT_2: 31;

 for n be Nat st 1 <= n < k1 holds (a . n) = (c . n)

 proof

 let n be Nat;

 assume 1 <= n < k1;

 then (a . n) = (b . n) & (b . n) = (c . n) by A16, A17, A20;

 hence thesis;

 end;

 hence thesis by A20, A16, A17, A21, LO;

 end;

 suppose

 A22: k1 > k2;

 k1 <= ( len a) by A16, FINSEQ_3: 25;

 then 1 <= k2 < ( len a) by A17, A22, FINSEQ_3: 25, XXREAL_0: 2;

 then

 A19: k2 in ( dom a) & [(a . k2), (c . k2)] in R by A16, A17, A22, FINSEQ_3: 25;

 for n be Nat st 1 <= n < k2 holds (a . n) = (c . n)

 proof

 let n be Nat;

 assume 1 <= n < k2;

 then (c . n) = (b . n) & 1 <= n < k1 by A17, A22, XXREAL_0: 2;

 hence thesis by A16;

 end;

 hence thesis by A17, A19, LO;

 end;

 end;

 end;

 end

 registration

 let I;

 let R be asymmetric Relation of I;

 cluster ( LexOrder (I,R)) -> asymmetric;

 coherence

 proof

 set Q = ( LexOrder (I,R));

 let a,b be object;

 assume a in ( field Q) & b in ( field Q);

 assume

 A1: [a, b] in Q & [b, a] in Q;

 then

 reconsider a, b as Element of (I * ) by ZFMISC_1: 87;

 set c = a;

 per cases by A1, LO;

 suppose a c< b & b c< c;

 hence thesis;

 end;

 suppose

 A2: a c< b & ex k be Nat st k in ( dom b) & k in ( dom c) & [(b . k), (c . k)] in R & for n be Nat st 1 <= n < k holds (b . n) = (c . n);

 then

 consider k be Nat such that

 A3: k in ( dom b) & k in ( dom c) & [(b . k), (c . k)] in R & for n be Nat st 1 <= n < k holds (b . n) = (c . n);

 [(a . k), (c . k)] in R by A2, A3, Lem12;

 hence thesis by PREFER_1: 22;

 end;

 suppose

 A12: b c< c & ex k be Nat st k in ( dom a) & k in ( dom b) & [(a . k), (b . k)] in R & for n be Nat st 1 <= n < k holds (a . n) = (b . n);

 then

 consider k be Nat such that

 A11: k in ( dom a) & k in ( dom b) & [(a . k), (b . k)] in R & for n be Nat st 1 <= n < k holds (a . n) = (b . n);

 k in ( dom c) & [(a . k), (c . k)] in R by A12, A11, Lem12;

 hence thesis by PREFER_1: 22;

 end;

 suppose

 A15: (ex k be Nat st k in ( dom a) & k in ( dom b) & [(a . k), (b . k)] in R & for n be Nat st 1 <= n < k holds (a . n) = (b . n)) & ex k be Nat st k in ( dom b) & k in ( dom c) & [(b . k), (c . k)] in R & for n be Nat st 1 <= n < k holds (b . n) = (c . n);

 then

 consider k1 be Nat such that

 A16: k1 in ( dom a) & k1 in ( dom b) & [(a . k1), (b . k1)] in R & for n be Nat st 1 <= n < k1 holds (a . n) = (b . n);

 consider k2 be Nat such that

 A17: k2 in ( dom b) & k2 in ( dom c) & [(b . k2), (c . k2)] in R & for n be Nat st 1 <= n < k2 holds (b . n) = (c . n) by A15;

 per cases by XXREAL_0: 1;

 suppose

 A18: k1 < k2;

 k2 <= ( len c) by A17, FINSEQ_3: 25;

 then 1 <= k1 < ( len c) by A16, A18, FINSEQ_3: 25, XXREAL_0: 2;

 then k1 in ( dom c) & [(a . k1), (c . k1)] in R by A16, A17, A18;

 hence thesis by PREFER_1: 22;

 end;

 suppose k1 = k2;

 hence thesis by A16, A17, PREFER_1: 22;

 end;

 suppose

 A22: k1 > k2;

 k1 <= ( len a) by A16, FINSEQ_3: 25;

 then 1 <= k2 < ( len a) by A17, A22, FINSEQ_3: 25, XXREAL_0: 2;

 then k2 in ( dom a) & [(a . k2), (c . k2)] in R by A16, A17, A22;

 hence thesis by PREFER_1: 22;

 end;

 end;

 end;

 end

 theorem :: BAGORD_2:60

 for R be asymmetric Relation of I holds for p,q,r be I -valued FinSequence holds [p, q] in ( LexOrder (I,R)) iff [(r ^ p), (r ^ q)] in ( LexOrder (I,R))

 proof

 let R be asymmetric Relation of I;

 let p,q,r be I -valued FinSequence;

 hereby

 assume [p, q] in ( LexOrder (I,R));

 per cases by LO;

 suppose p c< q;

 then (r ^ p) c= (r ^ q) & (r ^ p) <> (r ^ q) by FINSEQ_6: 13, FINSEQ_1: 33, XBOOLE_0:def 8;

 then (r ^ p) c< (r ^ q) by XBOOLE_0:def 8;

 hence [(r ^ p), (r ^ q)] in ( LexOrder (I,R)) by LO;

 end;

 suppose ex k be Nat st k in ( dom p) & k in ( dom q) & [(p . k), (q . k)] in R & for n be Nat st 1 <= n < k holds (p . n) = (q . n);

 then

 consider k be Nat such that

 A1: k in ( dom p) & k in ( dom q) & [(p . k), (q . k)] in R & for n be Nat st 1 <= n < k holds (p . n) = (q . n);

 set i = ( len r);

 set j = (i + k);



 A2: j in ( dom (r ^ p)) & j in ( dom (r ^ q)) by A1, FINSEQ_1: 28;



 A3: ((r ^ p) . j) = (p . k) & ((r ^ q) . j) = (q . k) by A1, FINSEQ_1:def 7;

 for n be Nat st 1 <= n < j holds ((r ^ p) . n) = ((r ^ q) . n)

 proof

 let n be Nat;

 assume

 A4: 1 <= n < j;

 per cases by NAT_1: 13;

 suppose n <= i;

 then n in ( dom r) by A4, FINSEQ_3: 25;

 then ((r ^ p) . n) = (r . n) = ((r ^ q) . n) by FINSEQ_1:def 7;

 hence thesis;

 end;

 suppose (i + 1) <= n;

 then

 consider m be Nat such that

 A5: n = ((i + 1) + m) by NAT_1: 10;



 A5A: n = (i + (1 + m)) by A5;

 then

 A6: 1 <= (1 + m) < k by A4, NAT_1: 11, XREAL_1: 6;

 k <= ( len p) & k <= ( len q) by A1, FINSEQ_3: 25;

 then 1 <= (1 + m) <= ( len p) & (1 + m) <= ( len q) by A6, XXREAL_0: 2;

 then (1 + m) in ( dom p) & (1 + m) in ( dom q) by FINSEQ_3: 25;

 then ((r ^ p) . n) = (p . (1 + m)) & ((r ^ q) . n) = (q . (1 + m)) by A5A, FINSEQ_1:def 7;

 hence thesis by A1, A6;

 end;

 end;

 hence [(r ^ p), (r ^ q)] in ( LexOrder (I,R)) by LO, A1, A2, A3;

 end;

 end;

 assume [(r ^ p), (r ^ q)] in ( LexOrder (I,R));

 per cases by LO;

 suppose (r ^ p) c< (r ^ q);

 then p c< q by Lem13;

 hence [p, q] in ( LexOrder (I,R)) by LO;

 end;

 suppose ex k be Nat st k in ( dom (r ^ p)) & k in ( dom (r ^ q)) & [((r ^ p) . k), ((r ^ q) . k)] in R & for n be Nat st 1 <= n < k holds ((r ^ p) . n) = ((r ^ q) . n);

 then

 consider k be Nat such that

 A1: k in ( dom (r ^ p)) & k in ( dom (r ^ q)) & [((r ^ p) . k), ((r ^ q) . k)] in R & for n be Nat st 1 <= n < k holds ((r ^ p) . n) = ((r ^ q) . n);

 set i = ( len r);



 A3: 1 <= k by A1, FINSEQ_3: 25;

 now

 assume k <= i;

 then k in ( dom r) by A3, FINSEQ_3: 25;

 then ((r ^ p) . k) = (r . k) = ((r ^ q) . k) by FINSEQ_1:def 7;

 hence contradiction by A1, PREFER_1: 22;

 end;

 then k >= (i + 1) by NAT_1: 13;

 then

 consider j be Nat such that

 A4: k = ((i + 1) + j) by NAT_1: 10;



 A5: k = (i + (1 + j)) by A4;

 k <= ( len (r ^ p)) = (i + ( len p)) & k <= ( len (r ^ q)) = (i + ( len q)) by A1, FINSEQ_3: 25, FINSEQ_1: 22;

 then

 A9: 1 <= (1 + j) <= ( len p) & (1 + j) <= ( len q) by A5, NAT_1: 11, XREAL_1: 6;

 then

 A6: (1 + j) in ( dom p) & (1 + j) in ( dom q) by FINSEQ_3: 25;

 then

 A7: ((r ^ p) . k) = (p . (1 + j)) & ((r ^ q) . k) = (q . (1 + j)) by A5, FINSEQ_1:def 7;

 for n be Nat st 1 <= n < (1 + j) holds (p . n) = (q . n)

 proof

 let n be Nat;

 assume

 A8: 1 <= n < (1 + j);

 then n < ( len p) & n < ( len q) by A9, XXREAL_0: 2;

 then n in ( dom p) & n in ( dom q) by A8, FINSEQ_3: 25;

 then (p . n) = ((r ^ p) . (i + n)) & (q . n) = ((r ^ q) . (i + n)) & 1 <= (i + n) < k by FINSEQ_1:def 7, NAT_1: 12, XREAL_1: 6, A5, A8;

 hence thesis by A1;

 end;

 hence thesis by LO, A1, A6, A7;

 end;

 end;

 definition

 let R;

 :: BAGORD_2:def15

 func PrecPrecM R -> strict RelExtension of ( finite-MultiSet_over the carrier of R) means

 : PPM: for m,n be Element of it holds m <= n iff [( OrderedPartition m), ( OrderedPartition n)] in ( LexOrder (the carrier of ( PrecM R),the InternalRel of ( PrecM R)));

 existence

 proof

 set I = the carrier of R;

 set M = ( finite-MultiSet_over I);

 defpred R[ bag of I, bag of I] means [( OrderedPartition $1), ( OrderedPartition $2)] in ( LexOrder (the carrier of ( PrecM R),the InternalRel of ( PrecM R)));

 consider N be strict RelExtension of M such that

 A1: for m,n be Element of N holds m <= n iff R[m, n] from RelEx;

 take N;

 thus thesis by A1;

 end;

 uniqueness

 proof

 let N1,N2 be strict RelExtension of ( finite-MultiSet_over the carrier of R) such that

 A1: for m,n be Element of N1 holds m <= n iff [( OrderedPartition m), ( OrderedPartition n)] in ( LexOrder (the carrier of ( PrecM R),the InternalRel of ( PrecM R))) and

 A2: for m,n be Element of N2 holds m <= n iff [( OrderedPartition m), ( OrderedPartition n)] in ( LexOrder (the carrier of ( PrecM R),the InternalRel of ( PrecM R)));

 for m,n be Element of N1 holds for x,y be Element of N2 st m = x & n = y holds m <= n iff x <= y

 proof

 let m,n be Element of N1;

 let k,l be Element of N2;

 assume

 Z0: m = k;

 assume

 Z1: n = l;

 m <= n iff [( OrderedPartition m), ( OrderedPartition n)] in ( LexOrder (the carrier of ( PrecM R),the InternalRel of ( PrecM R))) by A1;

 hence thesis by A2, Z0, Z1;

 end;

 hence thesis by Th4;

 end;

 end

 registration

 let R;

 cluster ( PrecPrecM R) -> asymmetric transitive;

 coherence

 proof

 set Q = the InternalRel of ( PrecPrecM R);

 thus ( PrecPrecM R) is asymmetric

 proof

 let a,b be object;

 assume a in the carrier of ( PrecPrecM R) & b in the carrier of ( PrecPrecM R);

 then

 reconsider m = a, n = b as Element of ( PrecPrecM R);

 assume [a, b] in Q & [b, a] in Q;

 then m <= n <= m by ORDERS_2:def 5;

 then [( OrderedPartition m), ( OrderedPartition n)] in ( LexOrder (the carrier of ( PrecM R),the InternalRel of ( PrecM R))) & [( OrderedPartition n), ( OrderedPartition m)] in ( LexOrder (the carrier of ( PrecM R),the InternalRel of ( PrecM R))) by PPM;

 hence thesis by PREFER_1: 22;

 end;

 let a,b,c be object;

 assume a in the carrier of ( PrecPrecM R) & b in the carrier of ( PrecPrecM R) & c in the carrier of ( PrecPrecM R);

 then

 reconsider m = a, n = b, o = c as Element of ( PrecPrecM R);

 assume [a, b] in Q & [b, c] in Q;

 then m <= n <= o by ORDERS_2:def 5;

 then [( OrderedPartition m), ( OrderedPartition n)] in ( LexOrder (the carrier of ( PrecM R),the InternalRel of ( PrecM R))) & [( OrderedPartition n), ( OrderedPartition o)] in ( LexOrder (the carrier of ( PrecM R),the InternalRel of ( PrecM R))) by PPM;

 then [( OrderedPartition m), ( OrderedPartition o)] in ( LexOrder (the carrier of ( PrecM R),the InternalRel of ( PrecM R))) by RELAT_2: 31;

 then m <= o by PPM;

 hence thesis by ORDERS_2:def 5;

 end;

 end

 theorem :: BAGORD_2:61

 for a,b be Element of ( DershowitzMannaOrder R) st a <= b holds b <> ( EmptyBag the carrier of R)

 proof

 set DM = ( DershowitzMannaOrder R);

 set I = the carrier of R;

 set E = ( EmptyBag I);

 let a,b be Element of DM;

 assume

 Z0: a <= b;

 per cases ;

 suppose a = E;

 hence b <> E by Z0;

 end;

 suppose

 A1: a <> E;

 E divides a by PRE_POLY: 59;

 then [E, a] in ( DivOrder I) c= the InternalRel of DM by A1, DO, Th16;

 hence thesis by Z0, ORDERS_2:def 5;

 end;

 end;

 theorem :: BAGORD_2:62

 for a,b,c,d be Element of ( DershowitzMannaOrder R) holds for e be bag of the carrier of R st a <= b & e divides a & e divides b holds c = (a -' e) & d = (b -' e) implies c <= d

 proof

 let a,b,c,d be Element of ( DershowitzMannaOrder R);

 let e be bag of the carrier of R;

 assume

 Z1: a <= b;

 assume

 Z2: e divides a;

 assume

 Z3: e divides b;

 assume

 Z4: c = (a -' e);

 assume d = (b -' e);

 then

 A0: a = (c + e) & b = (d + e) & a <> b by Z1, Z2, Z3, Z4, PRE_POLY: 47;

 for x st (c . x) > (d . x) holds ex y st x <= y & (c . y) < (d . y)

 proof

 let x;

 assume (c . x) > (d . x);

 then (a . x) = ((c . x) + (e . x)) > ((d . x) + (e . x)) = (b . x) by A0, PRE_POLY:def 5, XREAL_1: 6;

 then

 consider y such that

 A2: x <= y & (a . y) < (b . y) by Z1, HO;

 take y;

 (a . y) = ((c . y) + (e . y)) & (b . y) = ((d . y) + (e . y)) by A0, PRE_POLY:def 5;

 hence thesis by A2, XREAL_1: 6;

 end;

 hence c <= d by A0, HO;

 end;

 theorem :: BAGORD_2:63



 Lem14: for p be ( Bags I) -valued FinSequence, x be object st x in I & (( Sum p) . x) > 0 holds ex i be Nat st i in ( dom p) & ((p /. i) . x) > 0

 proof

 let p be ( Bags I) -valued FinSequence;

 let x be object;

 assume

 Z0: x in I;

 assume

 Z1: (( Sum p) . x) > 0 ;

 defpred P[ object] means for p be ( Bags I) -valued FinSequence st p = $1 & (( Sum p) . x) > 0 holds ex i be Nat st i in ( dom p) & ((p /. i) . x) > 0 ;



 A1: P[ {} ]

 proof

 let p be ( Bags I) -valued FinSequence;

 assume p = {} ;

 then p = ( <*> ( Bags I));

 then ( Sum p) = ( EmptyBag I) by Th21;

 hence thesis by Z0, FUNCOP_1: 7;

 end;



 A2: for p be FinSequence, a be object st P[p] holds P[(p ^ <*a*>)]

 proof

 let p be FinSequence;

 let a be object;

 assume

 Z0: P[p];

 let q be ( Bags I) -valued FinSequence;

 assume

 A3: q = (p ^ <*a*>);

 then

 reconsider p, aa = <*a*> as ( Bags I) -valued FinSequence by Lem8;

 ( len aa) = 1 by FINSEQ_1: 40;

 then 1 in ( dom aa) by FINSEQ_3: 25;

 then (aa . 1) in ( Bags I) by FUNCT_1: 102;

 then

 reconsider a as Element of ( Bags I) by FINSEQ_1: 40;

 assume (( Sum q) . x) > 0 ;

 then ((( Sum p) . x) + (a . x)) = ((( Sum p) + a) . x) > 0 by Th22, A3, PRE_POLY:def 5;

 per cases ;

 suppose

 A4: (a . x) > 0 ;

 take i = (( len p) + 1);

 ( len q) = (( len p) + 1) >= 1 by A3, NAT_1: 11, FINSEQ_2: 16;

 hence i in ( dom q) by FINSEQ_3: 25;

 then (q /. i) = (q . i) by PARTFUN1:def 6;

 hence thesis by A4, A3, FINSEQ_1: 42;

 end;

 suppose (( Sum p) . x) > 0 ;

 then

 consider i be Nat such that

 A5: i in ( dom p) & ((p /. i) . x) > 0 by Z0;

 take i;



 A6: ( dom p) c= ( dom q) by A3, FINSEQ_1: 26;

 hence i in ( dom q) by A5;

 (q /. i) = (q . i) = (p . i) by A3, A5, A6, FINSEQ_1:def 7, PARTFUN1:def 6;

 hence ((q /. i) . x) > 0 by PARTFUN1:def 6, A5;

 end;

 end;

 for p be FinSequence holds P[p] from FINSEQ_1:sch 3( A1, A2);

 hence thesis by Z1;

 end;

 theorem :: BAGORD_2:64

 q is ordered & ((q /. 1) . x) = 0 & (b . x) > 0 implies ex y st ((q /. 1) . y) > 0 & x <= y

 proof

 assume

 Z0: q is ordered;

 assume

 Z2: ((q /. 1) . x) = 0 ;

 assume

 Z3: (b . x) > 0 ;

 defpred P[ Nat] means $1 in ( dom q) implies for x st ((q /. $1) . x) > 0 holds ex y st ((q /. 1) . y) > 0 & x <= y;



 A1: P[2]

 proof

 assume

 A2: 2 in ( dom q);

 then 2 <= ( len q) by FINSEQ_3: 25;

 then 1 <= ( len q) by XXREAL_0: 2;

 then 1 in ( dom q) & 2 = (1 + 1) by FINSEQ_3: 25;

 hence thesis by A2, Z0;

 end;



 A3: for i be Nat st 2 <= i & P[i] holds P[(i + 1)]

 proof

 let i be Nat;

 assume

 A4: 2 <= i & P[i] & (i + 1) in ( dom q);

 then i <= (i + 1) <= ( len q) by NAT_1: 11, FINSEQ_3: 25;

 then

 A0: 1 <= i <= ( len q) by A4, XXREAL_0: 2;

 then

 A5: i in ( dom q) by FINSEQ_3: 25;

 let x;

 assume ((q /. (i + 1)) . x) > 0 ;

 then

 consider y such that

 A6: ((q /. i) . y) > 0 & x <= y by Z0, A4, A5;

 consider z such that

 A7: ((q /. 1) . z) > 0 & y <= z by A4, A0, A6, FINSEQ_3: 25;

 take z;

 thus ((q /. 1) . z) > 0 by A7;

 thus x <= z by A6, A7, ORDERS_2: 3;

 end;



 A8: for i be Nat st i >= 2 holds P[i] from NAT_1:sch 8( A1, A3);

 b = ( Sum q) by PART;

 then

 consider i be Nat such that

 A9: i in ( dom q) & ((q /. i) . x) > 0 by Z3, Lem14;

 1 <= i & i <> 1 by A9, Z2, FINSEQ_3: 25;

 then 1 < i by XXREAL_0: 1;

 then (1 + 1) <= i by NAT_1: 13;

 hence thesis by A8, A9;

 end;