defpred S1[ Ordinal] means InvLexOrder \$1 is well-ordering ;
A1: now :: thesis: for o being Ordinal st ( for n being Ordinal st n in o holds
S1[n] ) holds
S1[o]
let o be Ordinal; :: thesis: ( ( for n being Ordinal st n in o holds
S1[n] ) implies S1[o] )

assume A2: for n being Ordinal st n in o holds
S1[n] ; :: thesis: S1[o]
set ilo = InvLexOrder o;
A3: InvLexOrder o is_strongly_connected_in Bags o by Def5;
then InvLexOrder o is_reflexive_in Bags o ;
then A4: field () = Bags o by PARTIT_2:9;
A5: now :: thesis:
assume not InvLexOrder o is well_founded ; :: thesis: contradiction
then A6: not InvLexOrder o is_well_founded_in Bags o by ;
set R = RelStr(# (Bags o),() #);
set ir = the InternalRel of RelStr(# (Bags o),() #);
not RelStr(# (Bags o),() #) is well_founded by A6;
then consider f being sequence of RelStr(# (Bags o),() #) such that
A7: f is descending by WELLFND1:14;
reconsider a = f . 0 as bag of o ;
set s = SgmX ((),());
A8: field () = o by WELLORD2:def 1;
RelIncl o is being_linear-order by ORDERS_1:19;
then A9: RelIncl o linearly_orders support a by ;
then A10: rng (SgmX ((),())) = support a by PRE_POLY:def 2;
now :: thesis: not rng (SgmX ((),())) = {}
assume rng (SgmX ((),())) = {} ; :: thesis: contradiction
then A11: a = EmptyBag o by ;
reconsider b = f . (0 + 1) as bag of o ;
A12: b <> a by A7;
[b,a] in the InternalRel of RelStr(# (Bags o),() #) by A7;
then ex i being Ordinal st
( i in o & b . i < a . i & ( for k being Ordinal st i in k & k in o holds
b . k = a . k ) ) by ;
hence contradiction by A11, PBOOLE:5; :: thesis: verum
end;
then A13: len (SgmX ((),())) in dom (SgmX ((),())) by ;
then A14: (SgmX ((),())) . (len (SgmX ((),()))) in rng (SgmX ((),())) by FUNCT_1:3;
then reconsider j = (SgmX ((),())) . (len (SgmX ((),()))) as Ordinal by A10;
defpred S2[ set , set ] means ex b being bag of o st
( f . \$1 = b & \$2 = b . j );
A15: now :: thesis: for x being Element of NAT ex y being Element of omega st S2[x,y]
let x be Element of NAT ; :: thesis: ex y being Element of omega st S2[x,y]
reconsider b = f . x as bag of o ;
take y = b . j; :: thesis: S2[x,y]
thus S2[x,y] ; :: thesis: verum
end;
consider t being sequence of NAT such that
A16: for i being Element of NAT holds S2[i,t . i] from defpred S3[ Nat] means for i being Ordinal
for b being bag of o st j in i & i in o & f . \$1 = b holds
b . i = 0 ;
A17: S3[ 0 ]
proof
let i be Ordinal; :: thesis: for b being bag of o st j in i & i in o & f . 0 = b holds
b . i = 0

let b be bag of o; :: thesis: ( j in i & i in o & f . 0 = b implies b . i = 0 )
assume that
A18: j in i and
A19: i in o and
A20: f . 0 = b ; :: thesis: b . i = 0
assume b . i <> 0 ; :: thesis: contradiction
then i in support a by ;
then consider k being Nat such that
A21: k in dom (SgmX ((),())) and
A22: (SgmX ((),())) . k = i by ;
A23: k <= len (SgmX ((),())) by ;
per cases ( k = len (SgmX ((),())) or k < len (SgmX ((),())) ) by ;
suppose k = len (SgmX ((),())) ; :: thesis: contradiction
end;
suppose k < len (SgmX ((),())) ; :: thesis: contradiction
then [((SgmX ((),())) /. k),((SgmX ((),())) /. (len (SgmX ((),()))))] in RelIncl o by ;
then [((SgmX ((),())) . k),((SgmX ((),())) /. (len (SgmX ((),()))))] in RelIncl o by ;
then [((SgmX ((),())) . k),((SgmX ((),())) . (len (SgmX ((),()))))] in RelIncl o by ;
then (SgmX ((),())) . k c= (SgmX ((),())) . (len (SgmX ((),()))) by ;
hence contradiction by A18, A22, ORDINAL1:5; :: thesis: verum
end;
end;
end;
A24: for n being Nat st S3[n] holds
S3[n + 1]
proof
let n be Nat; :: thesis: ( S3[n] implies S3[n + 1] )
assume A25: for i being Ordinal
for b being bag of o st j in i & i in o & f . n = b holds
b . i = 0 ; :: thesis: S3[n + 1]
let i be Ordinal; :: thesis: for b being bag of o st j in i & i in o & f . (n + 1) = b holds
b . i = 0

let b1 be bag of o; :: thesis: ( j in i & i in o & f . (n + 1) = b1 implies b1 . i = 0 )
assume that
A26: j in i and
A27: i in o and
A28: f . (n + 1) = b1 ; :: thesis: b1 . i = 0
reconsider b = f . n as bag of o ;
A29: b . i = 0 by ;
A30: b1 <> b by ;
[b1,b] in InvLexOrder o by ;
then consider i1 being Ordinal such that
A31: i1 in o and
A32: b1 . i1 < b . i1 and
A33: for k being Ordinal st i1 in k & k in o holds
b1 . k = b . k by ;
per cases ( i1 in i or i1 = i or i in i1 ) by ORDINAL1:14;
suppose i1 in i ; :: thesis: b1 . i = 0
hence b1 . i = 0 by ; :: thesis: verum
end;
suppose i1 = i ; :: thesis: b1 . i = 0
hence b1 . i = 0 by A25, A26, A27, A32; :: thesis: verum
end;
suppose A34: i in i1 ; :: thesis: b1 . i = 0
assume b1 . i <> 0 ; :: thesis: contradiction
j in i1 by ;
hence contradiction by A25, A31, A32; :: thesis: verum
end;
end;
end;
A35: for n being Nat holds S3[n] from reconsider t = t as sequence of OrderedNAT by DICKSON:def 15;
A36: t is non-increasing
proof
let n be Nat; :: according to BAGORDER:def 3 :: thesis: [(t . (n + 1)),(t . n)] in the InternalRel of OrderedNAT
reconsider n0 = n as Element of NAT by ORDINAL1:def 12;
reconsider tn = t . n0, tn1 = t . (n0 + 1) as Nat ;
reconsider fn = f . n0, fn1 = f . (n0 + 1) as bag of o ;
A37: fn1 <> fn by A7;
[fn1,fn] in InvLexOrder o by A7;
then consider i being Ordinal such that
A38: i in o and
A39: fn1 . i < fn . i and
A40: for k being Ordinal st i in k & k in o holds
fn1 . k = fn . k by ;
A41: ex bn being bag of o st
( fn = bn & tn = bn . j ) by A16;
A42: ex bn1 being bag of o st
( fn1 = bn1 & tn1 = bn1 . j ) by A16;
now :: thesis: tn1 <= tn
per cases ( i = j or j in i or i in j ) by ORDINAL1:14;
suppose i = j ; :: thesis: tn1 <= tn
hence tn1 <= tn by ; :: thesis: verum
end;
suppose j in i ; :: thesis: tn1 <= tn
hence tn1 <= tn by ; :: thesis: verum
end;
suppose i in j ; :: thesis: tn1 <= tn
hence tn1 <= tn by A10, A14, A40, A41, A42; :: thesis: verum
end;
end;
end;
hence [(t . (n + 1)),(t . n)] in the InternalRel of OrderedNAT by ; :: thesis: verum
end;
set n = j;
set iln = InvLexOrder j;
set S = RelStr(# (Bags j),() #);
InvLexOrder j is_strongly_connected_in Bags j by Def5;
then InvLexOrder j is_reflexive_in Bags j ;
then A43: field () = Bags j by PARTIT_2:9;
consider p being Nat such that
A44: for r being Nat st p <= r holds
t . p = t . r by ;
defpred S4[ Nat, set ] means ex b being bag of o st
( b = f . (p + \$1) & \$2 = b | j );
A45: now :: thesis: for x being Element of NAT ex y being Element of Bags j st S4[x,y]
let x be Element of NAT ; :: thesis: ex y being Element of Bags j st S4[x,y]
reconsider b = f . (p + x) as bag of o ;
reconsider y = b | j as bag of j by ;
reconsider y = y as Element of Bags j by PRE_POLY:def 12;
take y = y; :: thesis: S4[x,y]
thus S4[x,y] ; :: thesis: verum
end;
consider g being sequence of (Bags j) such that
A46: for x being Element of NAT holds S4[x,g . x] from reconsider g = g as sequence of RelStr(# (Bags j),() #) ;
now :: thesis: for k being Nat holds
( g . (k + 1) <> g . k & [(g . (k + 1)),(g . k)] in InvLexOrder j )
let k be Nat; :: thesis: ( g . (k + 1) <> g . k & [(g . (k + 1)),(g . k)] in InvLexOrder j )
reconsider k0 = k as Element of NAT by ORDINAL1:def 12;
consider b being bag of o such that
A47: b = f . (p + k) and
A48: g . k0 = b | j by A46;
consider b1 being bag of o such that
A49: b1 = f . (p + (k + 1)) and
A50: g . (k + 1) = b1 | j by A46;
p + (k + 1) = (p + k) + 1 ;
then A51: b <> b1 by A7, A47, A49;
A52: ex bb being bag of o st
( f . (p + k) = bb & t . (p + k0) = bb . j ) by A16;
A53: ex bb1 being bag of o st
( f . (p + (k + 1)) = bb1 & t . (p + (k + 1)) = bb1 . j ) by A16;
A54: t . (p + k) = t . p by ;
thus g . (k + 1) <> g . k :: thesis: [(g . (k + 1)),(g . k)] in InvLexOrder j
proof
assume A55: not g . (k + 1) <> g . k ; :: thesis: contradiction
A56: o = dom b by PARTFUN1:def 2;
A57: o = dom b1 by PARTFUN1:def 2;
now :: thesis: for m being object st m in o holds
b . m = b1 . m
let m be object ; :: thesis: ( m in o implies b . b1 = b1 . b1 )
assume A58: m in o ; :: thesis: b . b1 = b1 . b1
reconsider mm = m as set by TARSKI:1;
per cases ( m in j or m = j or j in mm ) by ;
suppose A59: m in j ; :: thesis: b . b1 = b1 . b1
then (b | j) . m = b . m by FUNCT_1:49;
hence b . m = b1 . m by ; :: thesis: verum
end;
suppose m = j ; :: thesis: b . b1 = b1 . b1
hence b . m = b1 . m by ; :: thesis: verum
end;
suppose A60: j in mm ; :: thesis: b . b1 = b1 . b1
then b . m = 0 by ;
hence b . m = b1 . m by A35, A49, A58, A60; :: thesis: verum
end;
end;
end;
hence contradiction by A51, A56, A57, FUNCT_1:2; :: thesis: verum
end;
[(f . ((p + k) + 1)),(f . (p + k))] in InvLexOrder o by A7;
then consider i being Ordinal such that
A61: i in o and
A62: b1 . i < b . i and
A63: for k being Ordinal st i in k & k in o holds
b . k = b1 . k by ;
A64: now :: thesis: i in j
assume A65: not i in j ; :: thesis: contradiction
per cases ( i = j or j in i ) by ;
suppose A66: j in i ; :: thesis: contradiction
then b . i = 0 by
.= b1 . i by A35, A49, A61, A66 ;
hence contradiction by A62; :: thesis: verum
end;
end;
end;
reconsider bj = b | j, b1j = b1 | j as bag of j by ;
A67: b1j . i = b1 . i by ;
A68: bj . i = b . i by ;
now :: thesis: for k being Ordinal st i in k & k in j holds
bj . k = b1j . k
let k be Ordinal; :: thesis: ( i in k & k in j implies bj . k = b1j . k )
assume that
A69: i in k and
A70: k in j ; :: thesis: bj . k = b1j . k
k in o by ;
then A71: b . k = b1 . k by ;
thus bj . k = b . k by
.= b1j . k by ; :: thesis: verum
end;
hence [(g . (k + 1)),(g . k)] in InvLexOrder j by A48, A50, A62, A64, A67, A68, Def6; :: thesis: verum
end;
then g is descending ;
then not RelStr(# (Bags j),() #) is well_founded by WELLFND1:14;
then not InvLexOrder j is_well_founded_in the carrier of RelStr(# (Bags j),() #) ;
then not InvLexOrder j well_orders field () by ;
then not InvLexOrder j is well-ordering by WELLORD1:4;
hence contradiction by A2, A10, A14; :: thesis: verum
end;
A72: field () = Bags o by ORDERS_1:12;
then A73: InvLexOrder o is_reflexive_in Bags o by RELAT_2:def 9;
A74: InvLexOrder o is_transitive_in Bags o by ;
A75: InvLexOrder o is_antisymmetric_in Bags o by ;
A76: InvLexOrder o is_connected_in field () by A3, A4;
InvLexOrder o is_well_founded_in field () by ;
then InvLexOrder o well_orders field () by ;
hence S1[o] by WELLORD1:4; :: thesis: verum
end;
thus for o being Ordinal holds S1[o] from :: thesis: verum