defpred S_{1}[ Ordinal] means InvLexOrder $1 is well-ordering ;

_{1}[o]
from ORDINAL1:sch 2(A1); :: thesis: verum

A1: now :: thesis: for o being Ordinal st ( for n being Ordinal st n in o holds

S_{1}[n] ) holds

S_{1}[o]

thus
for o being Ordinal holds SS

S

let o be Ordinal; :: thesis: ( ( for n being Ordinal st n in o holds

S_{1}[n] ) implies S_{1}[o] )

assume A2: for n being Ordinal st n in o holds

S_{1}[n]
; :: thesis: S_{1}[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 (InvLexOrder o) = Bags o by PARTIT_2:9;

then A73: InvLexOrder o is_reflexive_in Bags o by RELAT_2:def 9;

A74: InvLexOrder o is_transitive_in Bags o by A72, RELAT_2:def 16;

A75: InvLexOrder o is_antisymmetric_in Bags o by A72, RELAT_2:def 12;

A76: InvLexOrder o is_connected_in field (InvLexOrder o) by A3, A4;

InvLexOrder o is_well_founded_in field (InvLexOrder o) by A5, WELLORD1:3;

then InvLexOrder o well_orders field (InvLexOrder o) by A4, A73, A74, A75, A76, WELLORD1:def 5;

hence S_{1}[o]
by WELLORD1:4; :: thesis: verum

end;S

assume A2: for n being Ordinal st n in o holds

S

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 (InvLexOrder o) = Bags o by PARTIT_2:9;

A5: now :: thesis: InvLexOrder o is well_founded

A72:
field (InvLexOrder o) = Bags o
by ORDERS_1:12;assume
not InvLexOrder o is well_founded
; :: thesis: contradiction

then A6: not InvLexOrder o is_well_founded_in Bags o by A4, WELLORD1:3;

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;

then consider f being sequence of RelStr(# (Bags o),(InvLexOrder o) #) such that

A7: f is descending by WELLFND1:14;

reconsider a = f . 0 as bag of o ;

set s = SgmX ((RelIncl o),(support a));

A8: field (RelIncl o) = o by WELLORD2:def 1;

RelIncl o is being_linear-order by ORDERS_1:19;

then A9: RelIncl o linearly_orders support a by A8, ORDERS_1:37, ORDERS_1:38;

then A10: rng (SgmX ((RelIncl o),(support a))) = support a by PRE_POLY:def 2;

then A14: (SgmX ((RelIncl o),(support a))) . (len (SgmX ((RelIncl o),(support a)))) in rng (SgmX ((RelIncl o),(support a))) by FUNCT_1:3;

then reconsider j = (SgmX ((RelIncl o),(support a))) . (len (SgmX ((RelIncl o),(support a)))) as Ordinal by A10;

defpred S_{2}[ set , set ] means ex b being bag of o st

( f . $1 = b & $2 = b . j );

A16: for i being Element of NAT holds S_{2}[i,t . i]
from FUNCT_2:sch 3(A15);

defpred S_{3}[ 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: S_{3}[ 0 ]
_{3}[n] holds

S_{3}[n + 1]
_{3}[n]
from NAT_1:sch 2(A17, A24);

reconsider t = t as sequence of OrderedNAT by DICKSON:def 15;

A36: t is non-increasing

set iln = InvLexOrder j;

set S = RelStr(# (Bags j),(InvLexOrder j) #);

InvLexOrder j is_strongly_connected_in Bags j by Def5;

then InvLexOrder j is_reflexive_in Bags j ;

then A43: field (InvLexOrder j) = 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 A36, Th9;

defpred S_{4}[ Nat, set ] means ex b being bag of o st

( b = f . (p + $1) & $2 = b | j );

A46: for x being Element of NAT holds S_{4}[x,g . x]
from FUNCT_2:sch 3(A45);

reconsider g = g as sequence of RelStr(# (Bags j),(InvLexOrder j) #) ;

then not RelStr(# (Bags j),(InvLexOrder j) #) is well_founded by WELLFND1:14;

then not InvLexOrder j is_well_founded_in the carrier of RelStr(# (Bags j),(InvLexOrder j) #) ;

then not InvLexOrder j well_orders field (InvLexOrder j) by A43, WELLORD1:def 5;

then not InvLexOrder j is well-ordering by WELLORD1:4;

hence contradiction by A2, A10, A14; :: thesis: verum

end;then A6: not InvLexOrder o is_well_founded_in Bags o by A4, WELLORD1:3;

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;

then consider f being sequence of RelStr(# (Bags o),(InvLexOrder o) #) such that

A7: f is descending by WELLFND1:14;

reconsider a = f . 0 as bag of o ;

set s = SgmX ((RelIncl o),(support a));

A8: field (RelIncl o) = o by WELLORD2:def 1;

RelIncl o is being_linear-order by ORDERS_1:19;

then A9: RelIncl o linearly_orders support a by A8, ORDERS_1:37, ORDERS_1:38;

then A10: rng (SgmX ((RelIncl o),(support a))) = support a by PRE_POLY:def 2;

now :: thesis: not rng (SgmX ((RelIncl o),(support a))) = {}

then A13:
len (SgmX ((RelIncl o),(support a))) in dom (SgmX ((RelIncl o),(support a)))
by FINSEQ_5:6, RELAT_1:38;assume
rng (SgmX ((RelIncl o),(support a))) = {}
; :: thesis: contradiction

then A11: a = EmptyBag o by A10, PRE_POLY:81;

reconsider b = f . (0 + 1) as bag of o ;

A12: b <> a by A7;

[b,a] in the InternalRel of RelStr(# (Bags o),(InvLexOrder 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 A12, Def6;

hence contradiction by A11, PBOOLE:5; :: thesis: verum

end;then A11: a = EmptyBag o by A10, PRE_POLY:81;

reconsider b = f . (0 + 1) as bag of o ;

A12: b <> a by A7;

[b,a] in the InternalRel of RelStr(# (Bags o),(InvLexOrder 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 A12, Def6;

hence contradiction by A11, PBOOLE:5; :: thesis: verum

then A14: (SgmX ((RelIncl o),(support a))) . (len (SgmX ((RelIncl o),(support a)))) in rng (SgmX ((RelIncl o),(support a))) by FUNCT_1:3;

then reconsider j = (SgmX ((RelIncl o),(support a))) . (len (SgmX ((RelIncl o),(support a)))) as Ordinal by A10;

defpred S

( f . $1 = b & $2 = b . j );

A15: now :: thesis: for x being Element of NAT ex y being Element of omega st S_{2}[x,y]

consider t being sequence of NAT such that let x be Element of NAT ; :: thesis: ex y being Element of omega st S_{2}[x,y]

reconsider b = f . x as bag of o ;

take y = b . j; :: thesis: S_{2}[x,y]

thus S_{2}[x,y]
; :: thesis: verum

end;reconsider b = f . x as bag of o ;

take y = b . j; :: thesis: S

thus S

A16: for i being Element of NAT holds S

defpred S

for b being bag of o st j in i & i in o & f . $1 = b holds

b . i = 0 ;

A17: S

proof

A24:
for n being Nat st S
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 A20, PRE_POLY:def 7;

then consider k being Nat such that

A21: k in dom (SgmX ((RelIncl o),(support a))) and

A22: (SgmX ((RelIncl o),(support a))) . k = i by A10, FINSEQ_2:10;

A23: k <= len (SgmX ((RelIncl o),(support a))) by A21, FINSEQ_3:25;

end;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 A20, PRE_POLY:def 7;

then consider k being Nat such that

A21: k in dom (SgmX ((RelIncl o),(support a))) and

A22: (SgmX ((RelIncl o),(support a))) . k = i by A10, FINSEQ_2:10;

A23: k <= len (SgmX ((RelIncl o),(support a))) by A21, FINSEQ_3:25;

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

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, A13, A21, PRE_POLY: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 6;

then [((SgmX ((RelIncl o),(support a))) . k),((SgmX ((RelIncl o),(support a))) . (len (SgmX ((RelIncl o),(support a)))))] in RelIncl o by A13, PARTFUN1:def 6;

then (SgmX ((RelIncl o),(support a))) . k c= (SgmX ((RelIncl o),(support a))) . (len (SgmX ((RelIncl o),(support a)))) by A10, A14, A19, A22, WELLORD2:def 1;

hence contradiction by A18, A22, ORDINAL1:5; :: thesis: verum

end;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 6;

then [((SgmX ((RelIncl o),(support a))) . k),((SgmX ((RelIncl o),(support a))) . (len (SgmX ((RelIncl o),(support a)))))] in RelIncl o by A13, PARTFUN1:def 6;

then (SgmX ((RelIncl o),(support a))) . k c= (SgmX ((RelIncl o),(support a))) . (len (SgmX ((RelIncl o),(support a)))) by A10, A14, A19, A22, WELLORD2:def 1;

hence contradiction by A18, A22, ORDINAL1:5; :: thesis: verum

S

proof

A35:
for n being Nat holds S
let n be Nat; :: thesis: ( S_{3}[n] implies S_{3}[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: S_{3}[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 A25, A26, A27;

A30: b1 <> b by A7, A28;

[b1,b] in InvLexOrder o by A7, A28;

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 A30, Def6;

end;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: S

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 A25, A26, A27;

A30: b1 <> b by A7, A28;

[b1,b] in InvLexOrder o by A7, A28;

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 A30, Def6;

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

end;

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

assume
b1 . i <> 0
; :: thesis: contradiction

j in i1 by A26, A34, ORDINAL1:10;

hence contradiction by A25, A31, A32; :: thesis: verum

end;j in i1 by A26, A34, ORDINAL1:10;

hence contradiction by A25, A31, A32; :: thesis: verum

reconsider t = t as sequence of OrderedNAT by DICKSON:def 15;

A36: t is non-increasing

proof

set n = j;
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 A37, Def6;

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;

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

end;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 A37, Def6;

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;

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

set iln = InvLexOrder j;

set S = RelStr(# (Bags j),(InvLexOrder j) #);

InvLexOrder j is_strongly_connected_in Bags j by Def5;

then InvLexOrder j is_reflexive_in Bags j ;

then A43: field (InvLexOrder j) = 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 A36, Th9;

defpred S

( b = f . (p + $1) & $2 = b | j );

A45: now :: thesis: for x being Element of NAT ex y being Element of Bags j st S_{4}[x,y]

consider g being sequence of (Bags j) such that let x be Element of NAT ; :: thesis: ex y being Element of Bags j st S_{4}[x,y]

reconsider b = f . (p + x) as bag of o ;

reconsider y = b | j as bag of j by A10, A14, Th17;

reconsider y = y as Element of Bags j by PRE_POLY:def 12;

take y = y; :: thesis: S_{4}[x,y]

thus S_{4}[x,y]
; :: thesis: verum

end;reconsider b = f . (p + x) as bag of o ;

reconsider y = b | j as bag of j by A10, A14, Th17;

reconsider y = y as Element of Bags j by PRE_POLY:def 12;

take y = y; :: thesis: S

thus S

A46: for x being Element of NAT holds S

reconsider g = g as sequence of RelStr(# (Bags j),(InvLexOrder j) #) ;

now :: thesis: for k being Nat holds

( g . (k + 1) <> g . k & [(g . (k + 1)),(g . k)] in InvLexOrder j )

then
g is descending
;( 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 A44, NAT_1:11;

thus g . (k + 1) <> g . k :: thesis: [(g . (k + 1)),(g . k)] in InvLexOrder j

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 A47, A49, A51, Def6;

A67: b1j . i = b1 . i by A64, FUNCT_1:49;

A68: bj . i = b . i by A64, FUNCT_1:49;

end;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 A44, NAT_1:11;

thus g . (k + 1) <> g . k :: thesis: [(g . (k + 1)),(g . k)] in InvLexOrder j

proof

[(f . ((p + k) + 1)),(f . (p + k))] in InvLexOrder o
by A7;
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;

end;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

hence
contradiction
by A51, A56, A57, FUNCT_1:2; :: thesis: verumb . m = b1 . m

let m be object ; :: thesis: ( m in o implies b . b_{1} = b1 . b_{1} )

assume A58: m in o ; :: thesis: b . b_{1} = b1 . b_{1}

reconsider mm = m as set by TARSKI:1;

end;assume A58: m in o ; :: thesis: b . b

reconsider mm = m as set by TARSKI:1;

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 A47, A49, A51, Def6;

A64: now :: thesis: i in j

reconsider bj = b | j, b1j = b1 | j as bag of j by A10, A14, Th17;assume A65:
not i in j
; :: thesis: contradiction

end;A67: b1j . i = b1 . i by A64, FUNCT_1:49;

A68: bj . i = b . i by A64, FUNCT_1:49;

now :: thesis: for k being Ordinal st i in k & k in j holds

bj . k = b1j . k

hence
[(g . (k + 1)),(g . k)] in InvLexOrder j
by A48, A50, A62, A64, A67, A68, Def6; :: thesis: verumbj . 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 A10, A14, A70, ORDINAL1:10;

then A71: b . k = b1 . k by A63, A69;

thus bj . k = b . k by A70, FUNCT_1:49

.= b1j . k by A70, A71, FUNCT_1:49 ; :: thesis: verum

end;assume that

A69: i in k and

A70: k in j ; :: thesis: bj . k = b1j . k

k in o by A10, A14, A70, ORDINAL1:10;

then A71: b . k = b1 . k by A63, A69;

thus bj . k = b . k by A70, FUNCT_1:49

.= b1j . k by A70, A71, FUNCT_1:49 ; :: thesis: verum

then not RelStr(# (Bags j),(InvLexOrder j) #) is well_founded by WELLFND1:14;

then not InvLexOrder j is_well_founded_in the carrier of RelStr(# (Bags j),(InvLexOrder j) #) ;

then not InvLexOrder j well_orders field (InvLexOrder j) by A43, WELLORD1:def 5;

then not InvLexOrder j is well-ordering by WELLORD1:4;

hence contradiction by A2, A10, A14; :: thesis: verum

then A73: InvLexOrder o is_reflexive_in Bags o by RELAT_2:def 9;

A74: InvLexOrder o is_transitive_in Bags o by A72, RELAT_2:def 16;

A75: InvLexOrder o is_antisymmetric_in Bags o by A72, RELAT_2:def 12;

A76: InvLexOrder o is_connected_in field (InvLexOrder o) by A3, A4;

InvLexOrder o is_well_founded_in field (InvLexOrder o) by A5, WELLORD1:3;

then InvLexOrder o well_orders field (InvLexOrder o) by A4, A73, A74, A75, A76, WELLORD1:def 5;

hence S