defpred S₁[ Ordinal] means InvLexOrder $1 is well-ordering ;

A1: now

let o be Ordinal; :: thesis: ( ( for n being Ordinal st n in o holds
S₁[n] ) implies S₁[o] )
assume A2: for n being Ordinal st n in o holds
S₁[n] ; :: thesis: S₁[o]
set ilo = InvLexOrder o;
A3: InvLexOrder o is_strongly_connected_in Bags o by Def7;
then InvLexOrder o is_reflexive_in Bags o by ORDERS_1:92;
then A4: field (InvLexOrder o) = Bags o by PARTIT_2:9;

A5: now

assume not InvLexOrder o is well_founded ; :: thesis: contradiction
then A6: not InvLexOrder o is_well_founded_in Bags o by A4, WELLORD1:5;
set R = RelStr(# (Bags o),(InvLexOrder o) #);
set ir = the InternalRel of RelStr(# (Bags o),(InvLexOrder o) #);
not RelStr(# (Bags o),(InvLexOrder o) #) is well_founded by A6, WELLFND1:def 2;
then consider f being sequence of RelStr(# (Bags o),(InvLexOrder o) #) such that
A7: f is descending by WELLFND1:15;
reconsider a = f . 0 as bag of by POLYNOM1:def 14;
set s = SgmX (RelIncl o),(support a);
A8: field (RelIncl o) = o by WELLORD2:def 1;
RelIncl o is well-ordering by WELLORD2:7;
then RelIncl o is being_linear-order by ORDERS_1:107;
then A9: RelIncl o linearly_orders support a by A8, ORDERS_1:133, ORDERS_1:134;
then A10: rng (SgmX (RelIncl o),(support a)) = support a by TRIANG_1:def 2;

now

assume rng (SgmX (RelIncl o),(support a)) = {} ; :: thesis: contradiction
then A11: a = EmptyBag o by A10, Th20;
reconsider b = f . (0 + 1) as bag of by POLYNOM1:def 14;
A12: b <> a by A7, WELLFND1:def 7;
[b,a] in the InternalRel of RelStr(# (Bags o),(InvLexOrder o) #) by A7, WELLFND1:def 7;
then consider i being Ordinal such that
i in o and
A13: b . i < a . i and
for k being Ordinal st i in k & k in o holds
b . k = a . k by A12, Def8;
thus contradiction by A11, A13, POLYNOM1:56; :: thesis: verum

end;

then A14: len (SgmX (RelIncl o),(support a)) in dom (SgmX (RelIncl o),(support a)) by FINSEQ_5:6, RELAT_1:60;
then A15: (SgmX (RelIncl o),(support a)) . (len (SgmX (RelIncl o),(support a))) in rng (SgmX (RelIncl o),(support a)) by FUNCT_1:12;
then reconsider j = (SgmX (RelIncl o),(support a)) . (len (SgmX (RelIncl o),(support a))) as Ordinal by A10;
defpred S₂[ set , set ] means ex b being bag of st
( f . $1 = b & $2 = b . j );

A16: now

let x be Element of NAT ; :: thesis: ex y being Element of NAT st S₂[x,y]
reconsider b = f . x as bag of by POLYNOM1:def 14;
take y = b . j; :: thesis: S₂[x,y]
thus S₂[x,y] ; :: thesis: verum

end;

consider t being Function of NAT ,NAT such that
A17: for i being Element of NAT holds S₂[i,t . i] from FUNCT_2:sch 3(A16);
defpred S₃[ Element of NAT ] means for i being Ordinal
for b being bag of st j in i & i in o & f . $1 = b holds
b . i = 0 ;
A18: for n being Element of NAT holds S₃[n]

proof

A19: S₃[ 0 ]

proof

let i be Ordinal; :: thesis: for b being bag of st j in i & i in o & f . 0 = b holds
b . i = 0
let b be bag of ; :: thesis: ( j in i & i in o & f . 0 = b implies b . i = 0 )
assume A20: ( j in i & i in o & f . 0 = b ) ; :: thesis: b . i = 0
assume b . i <> 0 ; :: thesis: contradiction
then i in support a by A20, POLYNOM1:def 7;
then consider k being Nat such that
A21: ( k in dom (SgmX (RelIncl o),(support a)) & (SgmX (RelIncl o),(support a)) . k = i ) by A10, FINSEQ_2:11;
A22: k <= len (SgmX (RelIncl o),(support a)) by A21, FINSEQ_3:27;

per cases ( k = len (SgmX (RelIncl o),(support a)) or k < len (SgmX (RelIncl o),(support a)) ) by A22, XXREAL_0:1;

suppose k = len (SgmX (RelIncl o),(support a)) ; :: thesis: contradiction

hence contradiction by A20, A21; :: thesis: verum

end;

suppose k < len (SgmX (RelIncl o),(support a)) ; :: thesis: contradiction

then [((SgmX (RelIncl o),(support a)) /. k),((SgmX (RelIncl o),(support a)) /. (len (SgmX (RelIncl o),(support a))))] in RelIncl o by A9, A14, A21, TRIANG_1:def 2;
then [((SgmX (RelIncl o),(support a)) . k),((SgmX (RelIncl o),(support a)) /. (len (SgmX (RelIncl o),(support a))))] in RelIncl o by A21, PARTFUN1:def 8;
then [((SgmX (RelIncl o),(support a)) . k),((SgmX (RelIncl o),(support a)) . (len (SgmX (RelIncl o),(support a))))] in RelIncl o by A14, PARTFUN1:def 8;
then (SgmX (RelIncl o),(support a)) . k c= (SgmX (RelIncl o),(support a)) . (len (SgmX (RelIncl o),(support a))) by A10, A15, A20, A21, WELLORD2:def 1;
hence contradiction by A20, A21, ORDINAL1:7; :: thesis: verum

end;

end;

end;

A23: for n being Element of NAT st S₃[n] holds
S₃[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₃[n] implies S₃[n + 1] )
assume A24: for i being Ordinal
for b being bag of st j in i & i in o & f . n = b holds
b . i = 0 ; :: thesis: S₃[n + 1]
let i be Ordinal; :: thesis: for b being bag of st j in i & i in o & f . (n + 1) = b holds
b . i = 0
let b1 be bag of ; :: thesis: ( j in i & i in o & f . (n + 1) = b1 implies b1 . i = 0 )
assume A25: ( j in i & i in o & f . (n + 1) = b1 ) ; :: thesis: b1 . i = 0
reconsider b = f . n as bag of by POLYNOM1:def 14;
A26: b . i = 0 by A24, A25;
( b1 <> b & [b1,b] in InvLexOrder o ) by A7, A25, WELLFND1:def 7;
then consider i1 being Ordinal such that
A27: i1 in o and
A28: b1 . i1 < b . i1 and
A29: for k being Ordinal st i1 in k & k in o holds
b1 . k = b . k by Def8;

per cases ( i1 in i or i1 = i or i in i1 ) by ORDINAL1:24;

suppose i1 in i ; :: thesis: b1 . i = 0

hence b1 . i = 0 by A25, A26, A29; :: thesis: verum

end;

suppose i1 = i ; :: thesis: b1 . i = 0

hence b1 . i = 0 by A24, A25, A28; :: thesis: verum

end;

suppose A30: i in i1 ; :: thesis: b1 . i = 0

assume b1 . i <> 0 ; :: thesis: contradiction
j in i1 by A25, A30, ORDINAL1:19;
hence contradiction by A24, A27, A28; :: thesis: verum

end;

end;

end;

thus for n being Element of NAT holds S₃[n] from NAT_1:sch 1(A19, A23); :: thesis: verum

end;

reconsider t = t as sequence of OrderedNAT by DICKSON:def 15;
A31: t is non-increasing

proof

let n be Element of NAT ; :: according to BAGORDER:def 3 :: thesis: [(t . (n + 1)),(t . n)] in the InternalRel of OrderedNAT
reconsider tn = t . n, tn1 = t . (n + 1) as Element of NAT by DICKSON:def 15;
reconsider fn = f . n, fn1 = f . (n + 1) as bag of by POLYNOM1:def 14;
A32: fn1 <> fn by A7, WELLFND1:def 7;
[fn1,fn] in InvLexOrder o by A7, WELLFND1:def 7;
then consider i being Ordinal such that
A33: i in o and
A34: fn1 . i < fn . i and
A35: for k being Ordinal st i in k & k in o holds
fn1 . k = fn . k by A32, Def8;
consider bn being bag of such that
A36: ( fn = bn & tn = bn . j ) by A17;
consider bn1 being bag of such that
A37: ( fn1 = bn1 & tn1 = bn1 . j ) by A17;

now

per cases ( i = j or j in i or i in j ) by ORDINAL1:24;

suppose i = j ; :: thesis: tn1 <= tn

hence tn1 <= tn by A34, A36, A37; :: thesis: verum

end;

suppose j in i ; :: thesis: tn1 <= tn

hence tn1 <= tn by A18, A33, A34; :: thesis: verum

end;

suppose i in j ; :: thesis: tn1 <= tn

hence tn1 <= tn by A10, A15, A35, A36, A37; :: thesis: verum

end;

end;

end;

hence [(t . (n + 1)),(t . n)] in the InternalRel of OrderedNAT by DICKSON:def 14, DICKSON:def 15; :: thesis: verum

end;

set n = j;
set iln = InvLexOrder j;
set S = RelStr(# (Bags j),(InvLexOrder j) #);
InvLexOrder j is_strongly_connected_in Bags j by Def7;
then InvLexOrder j is_reflexive_in Bags j by ORDERS_1:92;
then A38: field (InvLexOrder j) = Bags j by PARTIT_2:9;
consider p being Element of NAT such that
A39: for r being Element of NAT st p <= r holds
t . p = t . r by A31, Th11;
defpred S₄[ Element of NAT , set ] means ex b being bag of st
( b = f . (p + $1) & $2 = b | j );

A40: now

let x be Element of NAT ; :: thesis: ex y being Element of Bags j st S₄[x,y]
reconsider b = f . (p + x) as bag of by POLYNOM1:def 14;
reconsider y = b | j as bag of by A10, A15, Th21;
reconsider y = y as Element of Bags j by POLYNOM1:def 14;
take y = y; :: thesis: S₄[x,y]
thus S₄[x,y] ; :: thesis: verum

end;

consider g being Function of NAT ,(Bags j) such that
A41: for x being Element of NAT holds S₄[x,g . x] from FUNCT_2:sch 3(A40);
reconsider g = g as sequence of RelStr(# (Bags j),(InvLexOrder j) #) ;

now

let k be Element of NAT ; :: thesis: ( g . (k + 1) <> g . k & [(g . (k + 1)),(g . k)] in InvLexOrder j )
consider b being bag of such that
A42: ( b = f . (p + k) & g . k = b | j ) by A41;
consider b1 being bag of such that
A43: ( b1 = f . (p + (k + 1)) & g . (k + 1) = b1 | j ) by A41;
p + (k + 1) = (p + k) + 1 ;
then A44: b <> b1 by A7, A42, A43, WELLFND1:def 7;
consider bb being bag of such that
A45: ( f . (p + k) = bb & t . (p + k) = bb . j ) by A17;
consider bb1 being bag of such that
A46: ( f . (p + (k + 1)) = bb1 & t . (p + (k + 1)) = bb1 . j ) by A17;
A47: ( t . (p + k) = t . p & t . (p + (k + 1)) = t . p ) by A39, NAT_1:11;
thus g . (k + 1) <> g . k :: thesis: [(g . (k + 1)),(g . k)] in InvLexOrder j

proof

assume A48: not g . (k + 1) <> g . k ; :: thesis: contradiction
A49: ( o = dom b & o = dom b1 ) by PARTFUN1:def 4;

now

let m be set ; :: thesis: ( m in o implies b . b₁ = b1 . b₁ )
assume A50: m in o ; :: thesis: b . b₁ = b1 . b₁
A51: m is Ordinal by A50;

per cases ( m in j or m = j or j in m ) by A51, ORDINAL1:24;

suppose m in j ; :: thesis: b . b₁ = b1 . b₁

then ( (b | j) . m = b . m & (b1 | j) . m = b1 . m ) by FUNCT_1:72;
hence b . m = b1 . m by A42, A43, A48; :: thesis: verum

end;

suppose m = j ; :: thesis: b . b₁ = b1 . b₁

hence b . m = b1 . m by A42, A43, A45, A46, A47; :: thesis: verum

end;

suppose j in m ; :: thesis: b . b₁ = b1 . b₁

then ( b . m = 0 & b1 . m = 0 ) by A18, A42, A43, A50;
hence b . m = b1 . m ; :: thesis: verum

end;

end;

end;

hence contradiction by A44, A49, FUNCT_1:9; :: thesis: verum

end;

[(f . ((p + k) + 1)),(f . (p + k))] in InvLexOrder o by A7, WELLFND1:def 7;
then consider i being Ordinal such that
A52: i in o and
A53: b1 . i < b . i and
A54: for k being Ordinal st i in k & k in o holds
b . k = b1 . k by A42, A43, A44, Def8;

A55: now

assume A56: not i in j ; :: thesis: contradiction

per cases ( i = j or j in i ) by A56, ORDINAL1:24;

suppose i = j ; :: thesis: contradiction

hence contradiction by A42, A43, A45, A46, A47, A53; :: thesis: verum

end;

suppose A57: j in i ; :: thesis: contradiction

then b . i = 0 by A18, A42, A52
.= b1 . i by A18, A43, A52, A57 ;
hence contradiction by A53; :: thesis: verum

end;

end;

end;

reconsider bj = b | j, b1j = b1 | j as bag of by A10, A15, Th21;
A58: ( b1j . i = b1 . i & bj . i = b . i ) by A55, FUNCT_1:72;

now

let k be Ordinal; :: thesis: ( i in k & k in j implies bj . k = b1j . k )
assume A59: ( i in k & k in j ) ; :: thesis: bj . k = b1j . k
k in o by A10, A15, A59, ORDINAL1:19;
then A60: b . k = b1 . k by A54, A59;
thus bj . k = b . k by A59, FUNCT_1:72
.= b1j . k by A59, A60, FUNCT_1:72 ; :: thesis: verum

end;

hence [(g . (k + 1)),(g . k)] in InvLexOrder j by A42, A43, A53, A55, A58, Def8; :: thesis: verum

end;

then g is descending by WELLFND1:def 7;
then not RelStr(# (Bags j),(InvLexOrder j) #) is well_founded by WELLFND1:15;
then not InvLexOrder j is_well_founded_in the carrier of RelStr(# (Bags j),(InvLexOrder j) #) by WELLFND1:def 2;
then not InvLexOrder j well_orders field (InvLexOrder j) by A38, WELLORD1:def 5;
then not InvLexOrder j is well-ordering by WELLORD1:8;
hence contradiction by A2, A10, A15; :: thesis: verum

end;

A61: field (InvLexOrder o) = Bags o by ORDERS_1:97;
then A62: InvLexOrder o is_reflexive_in Bags o by RELAT_2:def 9;
A63: InvLexOrder o is_transitive_in Bags o by A61, RELAT_2:def 16;
A64: InvLexOrder o is_antisymmetric_in Bags o by A61, RELAT_2:def 12;
A65: InvLexOrder o is_connected_in field (InvLexOrder o) by A3, A4, ORDERS_1:92;
InvLexOrder o is_well_founded_in field (InvLexOrder o) by A5, WELLORD1:5;
then InvLexOrder o well_orders field (InvLexOrder o) by A4, A62, A63, A64, A65, WELLORD1:def 5;
hence S₁[o] by WELLORD1:8; :: thesis: verum

end;

thus for o being Ordinal holds S₁[o] from ORDINAL1:sch 2(A1); :: thesis: verum