let o be infinite Ordinal; :: thesis: not GrLexOrder o is well-ordering

set R = GrLexOrder o;

set r = RelStr(# (Bags o),(GrLexOrder o) #);

set ir = the InternalRel of RelStr(# (Bags o),(GrLexOrder o) #);

set cr = the carrier of RelStr(# (Bags o),(GrLexOrder o) #);

assume GrLexOrder o is well-ordering ; :: thesis: contradiction

then A1: GrLexOrder o is well_founded ;

the carrier of RelStr(# (Bags o),(GrLexOrder o) #) = field the InternalRel of RelStr(# (Bags o),(GrLexOrder o) #) by ORDERS_1:15;

then the InternalRel of RelStr(# (Bags o),(GrLexOrder o) #) is_well_founded_in the carrier of RelStr(# (Bags o),(GrLexOrder o) #) by A1, WELLORD1:3;

then A2: RelStr(# (Bags o),(GrLexOrder o) #) is well_founded ;

defpred S_{1}[ Nat, set ] means $2 = (o --> 0) +* ($1,1);

A9: for n being Element of NAT holds S_{1}[n,f . n]
from FUNCT_2:sch 3(A3);

reconsider f = f as sequence of RelStr(# (Bags o),(GrLexOrder o) #) ;

f is descending

set R = GrLexOrder o;

set r = RelStr(# (Bags o),(GrLexOrder o) #);

set ir = the InternalRel of RelStr(# (Bags o),(GrLexOrder o) #);

set cr = the carrier of RelStr(# (Bags o),(GrLexOrder o) #);

assume GrLexOrder o is well-ordering ; :: thesis: contradiction

then A1: GrLexOrder o is well_founded ;

the carrier of RelStr(# (Bags o),(GrLexOrder o) #) = field the InternalRel of RelStr(# (Bags o),(GrLexOrder o) #) by ORDERS_1:15;

then the InternalRel of RelStr(# (Bags o),(GrLexOrder o) #) is_well_founded_in the carrier of RelStr(# (Bags o),(GrLexOrder o) #) by A1, WELLORD1:3;

then A2: RelStr(# (Bags o),(GrLexOrder o) #) is well_founded ;

defpred S

A3: now :: thesis: for n being Element of NAT ex y being Element of the carrier of RelStr(# (Bags o),(GrLexOrder o) #) st S_{1}[n,y]

consider f being sequence of the carrier of RelStr(# (Bags o),(GrLexOrder o) #) such that let n be Element of NAT ; :: thesis: ex y being Element of the carrier of RelStr(# (Bags o),(GrLexOrder o) #) st S_{1}[n,y]

set y = (o --> 0) +* (n,1);

A4: dom (o --> 0) = o by FUNCOP_1:13;

reconsider y = (o --> 0) +* (n,1) as ManySortedSet of o ;

A5: omega c= o by CARD_3:85;

then y is finite-support by PRE_POLY:def 8;

then reconsider y = y as Element of the carrier of RelStr(# (Bags o),(GrLexOrder o) #) by PRE_POLY:def 12;

take y = y; :: thesis: S_{1}[n,y]

thus S_{1}[n,y]
; :: thesis: verum

end;set y = (o --> 0) +* (n,1);

A4: dom (o --> 0) = o by FUNCOP_1:13;

reconsider y = (o --> 0) +* (n,1) as ManySortedSet of o ;

A5: omega c= o by CARD_3:85;

now :: thesis: for x being object holds

( ( x in {n} implies y . x <> 0 ) & ( y . x <> 0 implies x in {n} ) )

then
support y = {n}
by PRE_POLY:def 7;( ( x in {n} implies y . x <> 0 ) & ( y . x <> 0 implies x in {n} ) )

let x be object ; :: thesis: ( ( x in {n} implies y . x <> 0 ) & ( y . x <> 0 implies x in {n} ) )

A6: y . x <> 0 and

A7: not x in {n} ; :: thesis: contradiction

x <> n by A7, TARSKI:def 1;

then A8: y . x = (o --> 0) . x by FUNCT_7:32;

end;hereby :: thesis: ( y . x <> 0 implies x in {n} )

assume that assume
x in {n}
; :: thesis: y . x <> 0

then x = n by TARSKI:def 1;

hence y . x <> 0 by A4, A5, FUNCT_7:31; :: thesis: verum

end;then x = n by TARSKI:def 1;

hence y . x <> 0 by A4, A5, FUNCT_7:31; :: thesis: verum

A6: y . x <> 0 and

A7: not x in {n} ; :: thesis: contradiction

x <> n by A7, TARSKI:def 1;

then A8: y . x = (o --> 0) . x by FUNCT_7:32;

then y is finite-support by PRE_POLY:def 8;

then reconsider y = y as Element of the carrier of RelStr(# (Bags o),(GrLexOrder o) #) by PRE_POLY:def 12;

take y = y; :: thesis: S

thus S

A9: for n being Element of NAT holds S

reconsider f = f as sequence of RelStr(# (Bags o),(GrLexOrder o) #) ;

f is descending

proof

hence
contradiction
by A2, WELLFND1:14; :: thesis: verum
let n be Nat; :: according to WELLFND1:def 6 :: thesis: ( not f . (n + 1) = f . n & [(f . (n + 1)),(f . n)] in the InternalRel of RelStr(# (Bags o),(GrLexOrder o) #) )

reconsider n0 = n as Element of NAT by ORDINAL1:def 12;

set fn1 = f . (n0 + 1);

set fn = f . n0;

A10: f . (n0 + 1) = (o --> 0) +* ((n + 1),1) by A9;

A11: f . n0 = (o --> 0) +* (n,1) by A9;

reconsider fn1 = f . (n0 + 1) as bag of o ;

reconsider fn = f . n0 as bag of o ;

A12: n0 in omega ;

A13: omega c= o by CARD_3:85;

n <> n + 1 ;

then A14: fn1 . n = (o --> 0) . n by A10, FUNCT_7:32

.= 0 by A12, A13, FUNCOP_1:7 ;

A15: dom (o --> 0) = o by FUNCOP_1:13;

then A16: fn . n = 1 by A11, A13, FUNCT_7:31;

thus f . (n + 1) <> f . n by A11, A13, A14, A15, FUNCT_7:31; :: thesis: [(f . (n + 1)),(f . n)] in the InternalRel of RelStr(# (Bags o),(GrLexOrder o) #)

fn1 <=' fn by A19, PRE_POLY:def 10;

then A20: [(f . (n + 1)),(f . n)] in LexOrder o by PRE_POLY:def 14;

consider tn being FinSequence of NAT such that

A21: TotDegree fn = Sum tn and

A22: tn = fn * (SgmX ((RelIncl o),(support fn))) by Def4;

consider tn1 being FinSequence of NAT such that

A23: TotDegree fn1 = Sum tn1 and

A24: tn1 = fn1 * (SgmX ((RelIncl o),(support fn1))) by Def4;

omega c= o by CARD_3:85;

then reconsider nn = n, n1n = n + 1 as Element of o by A12;

then A28: SgmX ((RelIncl o),(support fn1)) = <*n1n*> by Th10;

A29: dom fn = o by A11, A15, FUNCT_7:30;

A30: dom fn1 = o by A10, A15, FUNCT_7:30;

then SgmX ((RelIncl o),(support fn)) = <*nn*> by Th10;

then A32: tn = <*(fn . n)*> by A22, A29, FINSEQ_2:34

.= <*1*> by A11, A13, A15, FUNCT_7:31

.= <*(fn1 . n1n)*> by A10, A15, FUNCT_7:31

.= tn1 by A24, A28, A30, FINSEQ_2:34 ;

for a, b, c being bag of o st [a,b] in LexOrder o holds

[(a + c),(b + c)] in LexOrder o by Def5;

hence [(f . (n + 1)),(f . n)] in the InternalRel of RelStr(# (Bags o),(GrLexOrder o) #) by A20, A21, A23, A32, Def7; :: thesis: verum

end;reconsider n0 = n as Element of NAT by ORDINAL1:def 12;

set fn1 = f . (n0 + 1);

set fn = f . n0;

A10: f . (n0 + 1) = (o --> 0) +* ((n + 1),1) by A9;

A11: f . n0 = (o --> 0) +* (n,1) by A9;

reconsider fn1 = f . (n0 + 1) as bag of o ;

reconsider fn = f . n0 as bag of o ;

A12: n0 in omega ;

A13: omega c= o by CARD_3:85;

n <> n + 1 ;

then A14: fn1 . n = (o --> 0) . n by A10, FUNCT_7:32

.= 0 by A12, A13, FUNCOP_1:7 ;

A15: dom (o --> 0) = o by FUNCOP_1:13;

then A16: fn . n = 1 by A11, A13, FUNCT_7:31;

now :: thesis: for l being Ordinal st l in n holds

fn1 . l = fn . l

then A19:
fn1 < fn
by A14, A16, PRE_POLY:def 9;fn1 . l = fn . l

let l be Ordinal; :: thesis: ( l in n implies fn1 . l = fn . l )

assume A17: l in n ; :: thesis: fn1 . l = fn . l

then A18: l <> n ;

n < n + 1 by NAT_1:13;

then n in { i where i is Nat : i < n0 + 1 } ;

then n in n + 1 by AXIOMS:4;

then n c= n + 1 by ORDINAL1:def 2;

then l in n + 1 by A17;

then l <> n + 1 ;

hence fn1 . l = (o --> 0) . l by A10, FUNCT_7:32

.= fn . l by A11, A18, FUNCT_7:32 ;

:: thesis: verum

end;assume A17: l in n ; :: thesis: fn1 . l = fn . l

then A18: l <> n ;

n < n + 1 by NAT_1:13;

then n in { i where i is Nat : i < n0 + 1 } ;

then n in n + 1 by AXIOMS:4;

then n c= n + 1 by ORDINAL1:def 2;

then l in n + 1 by A17;

then l <> n + 1 ;

hence fn1 . l = (o --> 0) . l by A10, FUNCT_7:32

.= fn . l by A11, A18, FUNCT_7:32 ;

:: thesis: verum

thus f . (n + 1) <> f . n by A11, A13, A14, A15, FUNCT_7:31; :: thesis: [(f . (n + 1)),(f . n)] in the InternalRel of RelStr(# (Bags o),(GrLexOrder o) #)

fn1 <=' fn by A19, PRE_POLY:def 10;

then A20: [(f . (n + 1)),(f . n)] in LexOrder o by PRE_POLY:def 14;

consider tn being FinSequence of NAT such that

A21: TotDegree fn = Sum tn and

A22: tn = fn * (SgmX ((RelIncl o),(support fn))) by Def4;

consider tn1 being FinSequence of NAT such that

A23: TotDegree fn1 = Sum tn1 and

A24: tn1 = fn1 * (SgmX ((RelIncl o),(support fn1))) by Def4;

omega c= o by CARD_3:85;

then reconsider nn = n, n1n = n + 1 as Element of o by A12;

now :: thesis: for x being object holds

( ( x in support fn1 implies x in {n1n} ) & ( x in {n1n} implies x in support fn1 ) )

then
support fn1 = {n1n}
by TARSKI:2;( ( x in support fn1 implies x in {n1n} ) & ( x in {n1n} implies x in support fn1 ) )

let x be object ; :: thesis: ( ( x in support fn1 implies x in {n1n} ) & ( x in {n1n} implies x in support fn1 ) )

then x = n1n by TARSKI:def 1;

then fn1 . x = 1 by A10, A15, FUNCT_7:31;

hence x in support fn1 by PRE_POLY:def 7; :: thesis: verum

end;hereby :: thesis: ( x in {n1n} implies x in support fn1 )

assume
x in {n1n}
; :: thesis: x in support fn1assume A27:
x in support fn1
; :: thesis: x in {n1n}

end;now :: thesis: not x <> n1n

hence
x in {n1n}
by TARSKI:def 1; :: thesis: verumassume
x <> n1n
; :: thesis: contradiction

then fn1 . x = (o --> 0) . x by A10, FUNCT_7:32;

then fn1 . x = 0 by A27, FUNCOP_1:7;

hence contradiction by A27, PRE_POLY:def 7; :: thesis: verum

end;then fn1 . x = (o --> 0) . x by A10, FUNCT_7:32;

then fn1 . x = 0 by A27, FUNCOP_1:7;

hence contradiction by A27, PRE_POLY:def 7; :: thesis: verum

then x = n1n by TARSKI:def 1;

then fn1 . x = 1 by A10, A15, FUNCT_7:31;

hence x in support fn1 by PRE_POLY:def 7; :: thesis: verum

then A28: SgmX ((RelIncl o),(support fn1)) = <*n1n*> by Th10;

A29: dom fn = o by A11, A15, FUNCT_7:30;

A30: dom fn1 = o by A10, A15, FUNCT_7:30;

now :: thesis: for x being object holds

( ( x in support fn implies x in {nn} ) & ( x in {nn} implies x in support fn ) )

then
support fn = {nn}
by TARSKI:2;( ( x in support fn implies x in {nn} ) & ( x in {nn} implies x in support fn ) )

let x be object ; :: thesis: ( ( x in support fn implies x in {nn} ) & ( x in {nn} implies x in support fn ) )

then x = nn by TARSKI:def 1;

then fn . x = 1 by A11, A15, FUNCT_7:31;

hence x in support fn by PRE_POLY:def 7; :: thesis: verum

end;hereby :: thesis: ( x in {nn} implies x in support fn )

assume
x in {nn}
; :: thesis: x in support fnassume A31:
x in support fn
; :: thesis: x in {nn}

end;now :: thesis: not x <> nn

hence
x in {nn}
by TARSKI:def 1; :: thesis: verumassume
x <> nn
; :: thesis: contradiction

then fn . x = (o --> 0) . x by A11, FUNCT_7:32;

then fn . x = 0 by A31, FUNCOP_1:7;

hence contradiction by A31, PRE_POLY:def 7; :: thesis: verum

end;then fn . x = (o --> 0) . x by A11, FUNCT_7:32;

then fn . x = 0 by A31, FUNCOP_1:7;

hence contradiction by A31, PRE_POLY:def 7; :: thesis: verum

then x = nn by TARSKI:def 1;

then fn . x = 1 by A11, A15, FUNCT_7:31;

hence x in support fn by PRE_POLY:def 7; :: thesis: verum

then SgmX ((RelIncl o),(support fn)) = <*nn*> by Th10;

then A32: tn = <*(fn . n)*> by A22, A29, FINSEQ_2:34

.= <*1*> by A11, A13, A15, FUNCT_7:31

.= <*(fn1 . n1n)*> by A10, A15, FUNCT_7:31

.= tn1 by A24, A28, A30, FINSEQ_2:34 ;

for a, b, c being bag of o st [a,b] in LexOrder o holds

[(a + c),(b + c)] in LexOrder o by Def5;

hence [(f . (n + 1)),(f . n)] in the InternalRel of RelStr(# (Bags o),(GrLexOrder o) #) by A20, A21, A23, A32, Def7; :: thesis: verum