let o be infinite Ordinal; :: thesis:
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:
then A1: GrLexOrder o is well_founded by WELLORD1:def 4;
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 by WELLFND1:def 2;
defpred S₁[ Nat, set ] means $2 = (o --> 0) +* ($1,1);

A3: now

let n be Element of NAT ; :: thesis:
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: n in omega ;
A6: omega c= o by CARD_3:85;

now

let x be set ; :: thesis:

hereby :: thesis:

assume x in {n} ; :: thesis:
then x = n by TARSKI:def 1;
hence y . x <> 0 by A4, A5, A6, FUNCT_7:31; :: thesis:

end;

assume that
A7: y . x <> 0 and
A8: not x in {n} ; :: thesis:
x <> n by A8, TARSKI:def 1;
then A9: y . x = (o --> 0) . x by FUNCT_7:32;

per cases ;

suppose x in dom (o --> 0) ; :: thesis:

hence contradiction by A7, A9, FUNCOP_1:7; :: thesis:

end;

suppose not x in dom (o --> 0) ; :: thesis:

hence contradiction by A7, A9, FUNCT_1:def 2; :: thesis:

end;

end;

end;

then support y = {n} by PRE_POLY:def 7;
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:
thus S₁[n,y] ; :: thesis:

end;

consider f being Function of NAT, the carrier of RelStr(# (Bags o),(GrLexOrder o) #) such that
A10: for n being Element of NAT holds S₁[n,f . n] from FUNCT_2:sch 3(A3);
reconsider f = f as sequence of RelStr(# (Bags o),(GrLexOrder o) #) ;
f is descending

proof

let n be Nat; :: according to WELLFND1:def 6 :: thesis:
reconsider n0 = n as Element of NAT by ORDINAL1:def 12;
set fn1 = f . (n0 + 1);
set fn = f . n0;
A11: f . (n0 + 1) = (o --> 0) +* ((n + 1),1) by A10;
A12: f . n0 = (o --> 0) +* (n,1) by A10;
reconsider fn1 = f . (n0 + 1) as bag of o ;
reconsider fn = f . n0 as bag of o ;
A13: n0 in omega ;
A14: omega c= o by CARD_3:85;
n <> n + 1 ;
then A15: fn1 . n = (o --> 0) . n by A11, FUNCT_7:32
.= 0 by A13, A14, FUNCOP_1:7 ;
A16: dom (o --> 0) = o by FUNCOP_1:13;
then A17: fn . n = 1 by A12, A13, A14, FUNCT_7:31;

now

let l be Ordinal; :: thesis:
assume A18: l in n ; :: thesis:
then A19: l <> n ;
n < n + 1 by NAT_1:13;
then n in { i where i is Element of 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 A18;
then l <> n + 1 ;
hence fn1 . l = (o --> 0) . l by A11, FUNCT_7:32
.= fn . l by A12, A19, FUNCT_7:32 ;
:: thesis:

end;

then A20: fn1 < fn by A15, A17, PRE_POLY:def 9;
thus f . (n + 1) <> f . n by A12, A13, A14, A15, A16, FUNCT_7:31; :: thesis:
fn1 <=' fn by A20, PRE_POLY:def 10;
then A21: [(f . (n + 1)),(f . n)] in LexOrder o by PRE_POLY:def 14;
consider tn being FinSequence of NAT such that
A22: TotDegree fn = Sum tn and
A23: tn = fn * (SgmX ((RelIncl o),(support fn))) by Def4;
consider tn1 being FinSequence of NAT such that
A24: TotDegree fn1 = Sum tn1 and
A25: tn1 = fn1 * (SgmX ((RelIncl o),(support fn1))) by Def4;
A26: n + 1 in omega ;
omega c= o by CARD_3:85;
then reconsider nn = n, n1n = n + 1 as Element of o by A13, A26;
A27: field (RelIncl o) = o by WELLORD2:def 1;
RelIncl o is well-ordering by WELLORD2:6;
then A28: RelIncl o linearly_orders o by A27, ORDERS_1:19, ORDERS_1:37;

now

let x be set ; :: thesis:

hereby :: thesis:

assume A29: x in support fn1 ; :: thesis:

now

assume x <> n1n ; :: thesis:
then fn1 . x = (o --> 0) . x by A11, FUNCT_7:32;
then fn1 . x = 0 by A29, FUNCOP_1:7;
hence contradiction by A29, PRE_POLY:def 7; :: thesis:

end;

hence x in {n1n} by TARSKI:def 1; :: thesis:

end;

assume x in {n1n} ; :: thesis:
then x = n1n by TARSKI:def 1;
then fn1 . x = 1 by A11, A16, FUNCT_7:31;
hence x in support fn1 by PRE_POLY:def 7; :: thesis:

end;

then support fn1 = {n1n} by TARSKI:1;
then A30: SgmX ((RelIncl o),(support fn1)) = <*n1n*> by A28, Th12, ORDERS_1:38;
A31: dom fn = o by A12, A16, FUNCT_7:30;
A32: dom fn1 = o by A11, A16, FUNCT_7:30;

now

let x be set ; :: thesis:

hereby :: thesis:

assume A33: x in support fn ; :: thesis:

now

assume x <> nn ; :: thesis:
then fn . x = (o --> 0) . x by A12, FUNCT_7:32;
then fn . x = 0 by A33, FUNCOP_1:7;
hence contradiction by A33, PRE_POLY:def 7; :: thesis:

end;

hence x in {nn} by TARSKI:def 1; :: thesis:

end;

assume x in {nn} ; :: thesis:
then x = nn by TARSKI:def 1;
then fn . x = 1 by A12, A16, FUNCT_7:31;
hence x in support fn by PRE_POLY:def 7; :: thesis:

end;

then support fn = {nn} by TARSKI:1;
then SgmX ((RelIncl o),(support fn)) = <*nn*> by A28, Th12, ORDERS_1:38;
then A34: tn = <*(fn . n)*> by A23, A31, FINSEQ_2:34
.= <*1*> by A12, A13, A14, A16, FUNCT_7:31
.= <*(fn1 . n1n)*> by A11, A16, FUNCT_7:31
.= tn1 by A25, A30, A32, 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 Def7;
hence [(f . (n + 1)),(f . n)] in the InternalRel of RelStr(# (Bags o),(GrLexOrder o) #) by A21, A22, A24, A34, Def9; :: thesis:

end;

hence contradiction by A2, WELLFND1:14; :: thesis: