let F be Field; :: thesis: for m, n being Ordinal
for b being bag of n st support b = {m} holds
( len (divisors b) = (b . m) + 1 & ( for k being Nat
for S being finite Subset of n st S = {m} & k in dom (divisors b) holds
(divisors b) . k = (S,(k -' 1)) -bag ) )
let m, n be Ordinal; :: thesis: for b being bag of n st support b = {m} holds
( len (divisors b) = (b . m) + 1 & ( for k being Nat
for S being finite Subset of n st S = {m} & k in dom (divisors b) holds
(divisors b) . k = (S,(k -' 1)) -bag ) )
let b be bag of n; :: thesis: ( support b = {m} implies ( len (divisors b) = (b . m) + 1 & ( for k being Nat
for S being finite Subset of n st S = {m} & k in dom (divisors b) holds
(divisors b) . k = (S,(k -' 1)) -bag ) ) )
assume AS: support b = {m} ; :: thesis: ( len (divisors b) = (b . m) + 1 & ( for k being Nat
for S being finite Subset of n st S = {m} & k in dom (divisors b) holds
(divisors b) . k = (S,(k -' 1)) -bag ) )

per cases ( not m in n or m in n ) ;

suppose A: not m in n ; :: thesis: ( len (divisors b) = (b . m) + 1 & ( for k being Nat
for S being finite Subset of n st S = {m} & k in dom (divisors b) holds
(divisors b) . k = (S,(k -' 1)) -bag ) )

now :: thesis: for o being object st o in n holds
b . o = (EmptyBag n) . o

let o be object ; :: thesis: ( o in n implies b . o = (EmptyBag n) . o )
assume o in n ; :: thesis: b . o = (EmptyBag n) . o
then not o in support b by A, AS, TARSKI:def 1;
hence b . o = {} by PRE_POLY:def 7
.= (EmptyBag n) . o by PBOOLE:5 ;
:: thesis: verum

end;

then B: b = EmptyBag n by PBOOLE:def 10;
then C: b . m = 0 by PBOOLE:5;
D: divisors b = <*(EmptyBag n)*> by B, PRE_POLY:67;
then E: dom (divisors b) = {1} by FINSEQ_1:2, FINSEQ_1:38;
thus len (divisors b) = (b . m) + 1 by C, D, FINSEQ_1:40; :: thesis: for k being Nat
for S being finite Subset of n st S = {m} & k in dom (divisors b) holds
(divisors b) . k = (S,(k -' 1)) -bag

now :: thesis: for k being Nat
for S being finite Subset of n st S = {m} & k in dom (divisors b) holds
(divisors b) . k = (S,(k -' 1)) -bag

let k be Nat; :: thesis: for S being finite Subset of n st S = {m} & k in dom (divisors b) holds
(divisors b) . k = (S,(k -' 1)) -bag
let S be finite Subset of n; :: thesis: ( S = {m} & k in dom (divisors b) implies (divisors b) . k = (S,(k -' 1)) -bag )
assume H: ( S = {m} & k in dom (divisors b) ) ; :: thesis: (divisors b) . k = (S,(k -' 1)) -bag
then I: k = 1 by E, TARSKI:def 1;
then F: (divisors b) . k = EmptyBag n by D;
k -' 1 = k - 1 by H, E, XREAL_0:def 2;
hence (divisors b) . k = (S,(k -' 1)) -bag by F, I, UPROOTS:9; :: thesis: verum

end;

hence for k being Nat
for S being finite Subset of n st S = {m} & k in dom (divisors b) holds
(divisors b) . k = (S,(k -' 1)) -bag ; :: thesis: verum

end;

suppose m in n ; :: thesis: ( len (divisors b) = (b . m) + 1 & ( for k being Nat
for S being finite Subset of n st S = {m} & k in dom (divisors b) holds
(divisors b) . k = (S,(k -' 1)) -bag ) )

then for o being object st o in {m} holds
o in n by TARSKI:def 1;
then reconsider S = {m} as finite Subset of n by TARSKI:def 3;
deffunc H₁( Nat) -> Element of Bags n = (S,($1 -' 1)) -bag ;
consider F being FinSequence such that
A: ( len F = (b . m) + 1 & ( for k being Nat st k in dom F holds
F . k = H₁(k) ) ) from FINSEQ_1:sch 2();
set B = { ((S,i) -bag) where i is Element of NAT : i <= b . m } ;
F: { ((S,i) -bag) where i is Element of NAT : i <= b . m } is finite

proof

defpred S₁[ set ] means 1 = 1;
set G = { H₁(i) where i is Nat : ( i <= (b . m) + 1 & S₁[i] ) } ;
H: { H₁(i) where i is Nat : ( i <= (b . m) + 1 & S₁[i] ) } is finite from FINSEQ_1:sch 6();
{ ((S,i) -bag) where i is Element of NAT : i <= b . m } c= { H₁(i) where i is Nat : ( i <= (b . m) + 1 & S₁[i] ) }

proof

now :: thesis: for o being object st o in { ((S,i) -bag) where i is Element of NAT : i <= b . m } holds
o in { H₁(i) where i is Nat : ( i <= (b . m) + 1 & S₁[i] ) }

let o be object ; :: thesis: ( o in { ((S,i) -bag) where i is Element of NAT : i <= b . m } implies o in { H₁(i) where i is Nat : ( i <= (b . m) + 1 & S₁[i] ) } )
assume o in { ((S,i) -bag) where i is Element of NAT : i <= b . m } ; :: thesis: o in { H₁(i) where i is Nat : ( i <= (b . m) + 1 & S₁[i] ) }
then consider i being Element of NAT such that
H1: ( o = (S,i) -bag & i <= b . m ) ;
H2: i + 1 <= (b . m) + 1 by H1, XREAL_1:6;
(i + 1) -' 1 = (i + 1) - 1 by XREAL_0:def 2;
hence o in { H₁(i) where i is Nat : ( i <= (b . m) + 1 & S₁[i] ) } by H1, H2; :: thesis: verum

end;

hence { ((S,i) -bag) where i is Element of NAT : i <= b . m } c= { H₁(i) where i is Nat : ( i <= (b . m) + 1 & S₁[i] ) } ; :: thesis: verum

end;

hence { ((S,i) -bag) where i is Element of NAT : i <= b . m } is finite by H; :: thesis: verum

end;

G: { ((S,i) -bag) where i is Element of NAT : i <= b . m } c= Bags n

proof

now :: thesis: for o being object st o in { ((S,i) -bag) where i is Element of NAT : i <= b . m } holds
o in Bags n

let o be object ; :: thesis: ( o in { ((S,i) -bag) where i is Element of NAT : i <= b . m } implies o in Bags n )
assume o in { ((S,i) -bag) where i is Element of NAT : i <= b . m } ; :: thesis: o in Bags n
then consider i being Element of NAT such that
H1: ( o = (S,i) -bag & i <= b . m ) ;
thus o in Bags n by H1; :: thesis: verum

end;

hence { ((S,i) -bag) where i is Element of NAT : i <= b . m } c= Bags n ; :: thesis: verum

end;

(S,0) -bag in { ((S,i) -bag) where i is Element of NAT : i <= b . m } ;
then reconsider B = { ((S,i) -bag) where i is Element of NAT : i <= b . m } as non empty finite Subset of (Bags n) by F, G;
D: rng F = B

proof

D0: now :: thesis: for o being object st o in rng F holds
o in B

let o be object ; :: thesis: ( o in rng F implies o in B )
assume o in rng F ; :: thesis: o in B
then consider i being Nat such that
D1: ( i in dom F & F . i = o ) by FINSEQ_2:10;
D2: o = (S,(i -' 1)) -bag by D1, A;
dom F = Seg (len F) by FINSEQ_1:def 3;
then D3: ( 1 <= i & i <= (b . m) + 1 ) by D1, A, FINSEQ_1:1;
then D4: i - 1 <= ((b . m) + 1) - 1 by XREAL_1:9;
i - 1 = i -' 1 by D3, XREAL_0:def 2;
hence o in B by D2, D4; :: thesis: verum

end;

now :: thesis: for o being object st o in B holds
o in rng F

let o be object ; :: thesis: ( o in B implies o in rng F )
assume o in B ; :: thesis: o in rng F
then consider i being Element of NAT such that
D1: ( o = (S,i) -bag & i <= b . m ) ;
D2: (i + 1) -' 1 = (i + 1) - 1 by XREAL_0:def 2;
( 1 <= i + 1 & i + 1 <= (b . m) + 1 ) by D1, XREAL_1:6, NAT_1:11;
then i + 1 in Seg (len F) by A;
then D3: i + 1 in dom F by FINSEQ_1:def 3;
then F . (i + 1) = o by A, D2, D1;
hence o in rng F by D3, FUNCT_1:def 3; :: thesis: verum

end;

hence rng F = B by D0, TARSKI:2; :: thesis: verum

end;

then reconsider F = F as FinSequence of Bags n by FINSEQ_1:def 4;
field (BagOrder n) = Bags n by ORDERS_1:12;
then C: BagOrder n linearly_orders B by ORDERS_1:37, ORDERS_1:38;
for x, y being Nat st x in dom F & y in dom F & x < y holds
( F /. x <> F /. y & [(F /. x),(F /. y)] in BagOrder n )

proof

let x, y be Nat; :: thesis: ( x in dom F & y in dom F & x < y implies ( F /. x <> F /. y & [(F /. x),(F /. y)] in BagOrder n ) )
assume C1: ( x in dom F & y in dom F & x < y ) ; :: thesis: ( F /. x <> F /. y & [(F /. x),(F /. y)] in BagOrder n )
then C2: ( F /. x = F . x & F /. y = F . y ) by PARTFUN1:def 6;
dom F = Seg (len F) by FINSEQ_1:def 3;
then ( 1 <= x & 1 <= y ) by C1, FINSEQ_1:1;
then C4: ( x -' 1 = x - 1 & y -' 1 = y - 1 ) by XREAL_0:def 2;
then C7: x -' 1 < y -' 1 by C1, XREAL_1:9;
C5: ( F . x = (S,(x -' 1)) -bag & F . y = (S,(y -' 1)) -bag ) by C1, A;
C6: m in {m} by TARSKI:def 1;
thus F /. x <> F /. y :: thesis: [(F /. x),(F /. y)] in BagOrder n

proof

( (F . x) . m = x -' 1 & (F . y) . m = y -' 1 ) by C5, C6, UPROOTS:7;
hence F /. x <> F /. y by C4, C2, C1; :: thesis: verum

end;

thus [(F /. x),(F /. y)] in BagOrder n :: thesis: verum

proof

(S,(x -' 1)) -bag <=' (S,(y -' 1)) -bag

proof

per cases ( x -' 1 = 0 or x -' 1 <> 0 ) ;

suppose x -' 1 = 0 ; :: thesis: (S,(x -' 1)) -bag <=' (S,(y -' 1)) -bag

then (S,(x -' 1)) -bag = EmptyBag n by UPROOTS:9;
hence (S,(x -' 1)) -bag <=' (S,(y -' 1)) -bag by PRE_POLY:60; :: thesis: verum

end;

suppose x -' 1 <> 0 ; :: thesis: (S,(x -' 1)) -bag <=' (S,(y -' 1)) -bag

then D2: support ((S,(x -' 1)) -bag) = {m} by UPROOTS:8;
D3: ((S,(x -' 1)) -bag) . m = x -' 1 by C6, UPROOTS:7;
D4: support ((S,(y -' 1)) -bag) = {m} by C7, UPROOTS:8;
((S,(y -' 1)) -bag) . m = y -' 1 by C6, UPROOTS:7;
hence (S,(x -' 1)) -bag <=' (S,(y -' 1)) -bag by C7, D2, D3, D4, Th13e; :: thesis: verum

end;

end;

end;

hence [(F /. x),(F /. y)] in BagOrder n by C2, C5, PRE_POLY:def 14; :: thesis: verum

end;

end;

then B: F = SgmX ((BagOrder n),B) by C, D, PRE_POLY:def 2;
H: for p being bag of n holds
( p in B iff p divides b )

proof

let p be bag of n; :: thesis: ( p in B iff p divides b )

B1: now :: thesis: ( p in B implies p divides b )

assume p in B ; :: thesis: p divides b
then consider i being Element of NAT such that
B2: ( p = (S,i) -bag & i <= b . m ) ;

per cases ( i = 0 or i <> 0 ) ;

suppose i = 0 ; :: thesis: p divides b

then (S,i) -bag = EmptyBag n by UPROOTS:9;
hence p divides b by B2, PRE_POLY:59; :: thesis: verum

end;

suppose i <> 0 ; :: thesis: p divides b

then B3: support ((S,i) -bag) = {m} by UPROOTS:8;

now :: thesis: for k being object holds p . k <= b . k

let k be object ; :: thesis: p . b₁ <= b . b₁

per cases ( k = m or k <> m ) ;

suppose B4: k = m ; :: thesis: p . b₁ <= b . b₁

m in {m} by TARSKI:def 1;
hence p . k <= b . k by B2, B4, UPROOTS:7; :: thesis: verum

end;

suppose k <> m ; :: thesis: p . b₁ <= b . b₁

then not k in support p by B2, B3, TARSKI:def 1;
hence p . k <= b . k by PRE_POLY:def 7; :: thesis: verum

end;

end;

end;

hence p divides b by PRE_POLY:def 11; :: thesis: verum

end;

end;

end;

now :: thesis: ( p divides b implies p in B )

assume p divides b ; :: thesis: p in B

per cases then ( p = EmptyBag n or ( support p = {m} & p . m <= b . m ) ) by AS, Th13h;

suppose p = EmptyBag n ; :: thesis: p in B

then p = (S,0) -bag by UPROOTS:9;
hence p in B ; :: thesis: verum

end;

suppose B2: ( support p = {m} & p . m <= b . m ) ; :: thesis: p in B

p = (S,(p . m)) -bag

proof

now :: thesis: for o being object st o in n holds
p . o = ((S,(p . m)) -bag) . o

let o be object ; :: thesis: ( o in n implies p . b₁ = ((S,(p . m)) -bag) . b₁ )
assume o in n ; :: thesis: p . b₁ = ((S,(p . m)) -bag) . b₁

per cases ( o in support p or not o in support p ) ;

suppose o in support p ; :: thesis: p . b₁ = ((S,(p . m)) -bag) . b₁

then B3: o = m by B2, TARSKI:def 1;
m in {m} by TARSKI:def 1;
hence p . o = ((S,(p . m)) -bag) . o by B3, UPROOTS:7; :: thesis: verum

end;

suppose B3: not o in support p ; :: thesis: p . b₁ = ((S,(p . m)) -bag) . b₁

hence p . o = 0 by PRE_POLY:def 7
.= ((S,(p . m)) -bag) . o by B3, B2, UPROOTS:6 ;
:: thesis: verum

end;

end;

end;

hence p = (S,(p . m)) -bag by PBOOLE:3; :: thesis: verum

end;

hence p in B by B2; :: thesis: verum

end;

end;

end;

hence ( p in B iff p divides b ) by B1; :: thesis: verum

end;

then E: F = divisors b by B, PRE_POLY:def 16;
thus len (divisors b) = (b . m) + 1 by A, B, H, PRE_POLY:def 16; :: thesis: for k being Nat
for S being finite Subset of n st S = {m} & k in dom (divisors b) holds
(divisors b) . k = (S,(k -' 1)) -bag
thus for k being Nat
for S being finite Subset of n st S = {m} & k in dom (divisors b) holds
(divisors b) . k = (S,(k -' 1)) -bag by A, E; :: thesis: verum

end;

end;