let T be reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TAS-structure ; :: thesis:
let t1, t2 be type of T; :: thesis:
set R = T @--> ;
given p being RedSequence of T @--> such that A1: ( p . 1 = t1 & t2 = p . (len p) ) ; :: according to REWRITE1:def 3 :: thesis:
A2: len p >= 0 + 1 by NAT_1:13;
then consider i being Nat such that
A3: len p = 1 + i by NAT_1:10;
reconsider i = i as Element of NAT by ORDINAL1:def 13;
defpred S₁[ set , set ] means ex j being Element of NAT ex a being adjective of T ex t being type of T st
( $2 = a & $1 = j & a ast t = p . j & t = p . (j + 1) & a is_properly_applicable_to t );

A4: now

let x be set ; :: thesis:
assume A5: x in Seg i ; :: thesis:
then reconsider j = x as Element of NAT ;
A6: ( j >= 1 & j <= i ) by A5, FINSEQ_1:3;
then ( 1 <= j + 1 & j + 1 <= len p & j < len p ) by A3, NAT_1:13, XREAL_1:8;
then ( j in dom p & j + 1 in dom p ) by A6, FINSEQ_3:27;
then A7: [(p . j),(p . (j + 1))] in T @--> by REWRITE1:def 2;
then reconsider q1 = p . j, q2 = p . (j + 1) as type of T by ZFMISC_1:106;
ex a being adjective of T st
( not a in adjs q2 & a is_properly_applicable_to q2 & a ast q2 = q1 ) by A7, Def31;
hence ex y being set st
( y in the adjectives of T & S₁[x,y] ) ; :: thesis:

end;

consider f being Function such that
A8: ( dom f = Seg i & rng f c= the adjectives of T ) and
A9: for x being set st x in Seg i holds
S₁[x,f . x] from WELLORD2:sch 1(A4);
f is FinSequence by A8, FINSEQ_1:def 2;
then reconsider f = f as FinSequence of the adjectives of T by A8, FINSEQ_1:def 4;
set r = Rev f;
defpred S₂[ Element of NAT ] means ( 1 + $1 <= len p implies (Rev p) . (1 + $1) = (apply (Rev f),t2) . (1 + $1) );
A10: ( len (Rev f) = len f & len (apply (Rev f),t2) = (len (Rev f)) + 1 & len f = i & len (Rev p) = len p ) by A8, Def19, FINSEQ_1:def 3, FINSEQ_5:def 3;
then ( 1 in dom (Rev p) & ((len p) - 1) + 1 = len p ) by A2, FINSEQ_3:27;
then (Rev p) . 1 = t2 by A1, FINSEQ_5:def 3;
then A11: S₂[ 0 ] by Def19;

A12: now

let j be Element of NAT ; :: thesis:
assume A13: S₂[j] ; :: thesis:

now

assume A14: 1 + (j + 1) <= len p ; :: thesis:
then j + 1 <= i by A3, XREAL_1:8;
then consider x being Nat such that
A15: i = (j + 1) + x by NAT_1:10;
reconsider x = x as Element of NAT by ORDINAL1:def 13;
A16: i = (x + 1) + j by A15;
then ( x + 1 >= 1 & i >= x + 1 ) by NAT_1:11;
then x + 1 in Seg i ;
then consider k being Element of NAT , a being adjective of T, t being type of T such that
A17: ( f . (x + 1) = a & x + 1 = k & a ast t = p . k & t = p . (k + 1) & a is_properly_applicable_to t ) by A9;
A18: (i + 1) - (j + 1) = x + 1 by A15;
A19: (i + 1) - (1 + (j + 1)) = x by A15;
j <= i by A16, NAT_1:11;
then ( j + 1 >= 1 & j + 1 <= i & j + 1 <= i + 1 ) by A15, NAT_1:11, XREAL_1:8;
then A20: ( j + 1 in dom (Rev f) & j + 1 in dom (apply (Rev f),t2) ) by A10, FINSEQ_3:27;
( 1 + (j + 1) >= 1 & j + 1 >= 1 & j + 1 < len p ) by A14, NAT_1:11, NAT_1:13;
then ( j + 1 in dom (Rev p) & 1 + (j + 1) in dom (Rev p) & (Rev p) . (1 + j) = (apply (Rev f),t2) . (1 + j) ) by A10, A13, A14, FINSEQ_3:27;
then A21: ( (Rev p) . (j + 1) = p . ((x + 1) + 1) & (Rev p) . (1 + (j + 1)) = p . (x + 1) ) by A3, A18, A19, FINSEQ_5:def 3;
(Rev f) . (j + 1) = f . (((len f) - (j + 1)) + 1) by A20, FINSEQ_5:def 3
.= a by A10, A15, A17 ;
hence (Rev p) . (1 + (j + 1)) = (apply (Rev f),t2) . (1 + (j + 1)) by A13, A14, A17, A20, A21, Def19, NAT_1:13; :: thesis:

end;

hence S₂[j + 1] ; :: thesis:

end;

A22: for j being Element of NAT holds S₂[j] from NAT_1:sch 1(A11, A12);

now

let j be Nat; :: thesis:
assume 1 <= j ; :: thesis:
then consider k being Nat such that
A23: j = 1 + k by NAT_1:10;
k in NAT by ORDINAL1:def 13;
hence ( j <= len p implies (Rev p) . j = (apply (Rev f),t2) . j ) by A22, A23; :: thesis:

end;

then A24: Rev p = apply (Rev f),t2 by A3, A10, FINSEQ_1:18;
then A25: p = Rev (apply (Rev f),t2) by FINSEQ_6:29;
reconsider A = rng f as finite Subset of the adjectives of T ;
take A ; :: thesis:
A26: Rev f is_properly_applicable_to t2

proof

let j be natural number ; :: according to ABCMIZ_0:def 28 :: thesis:
let a be adjective of T; :: thesis:
let s be type of T; :: thesis:
assume A27: ( j in dom (Rev f) & a = (Rev f) . j & s = (apply (Rev f),t2) . j ) ; :: thesis:
then ( j in dom f & j >= 1 & j <= len (Rev f) ) by FINSEQ_3:27, FINSEQ_5:60;
then consider k being Nat such that
A28: len (Rev f) = j + k by NAT_1:10;
reconsider k = k as Element of NAT by ORDINAL1:def 13;
A29: len (Rev f) = len f by FINSEQ_5:def 3;
then A30: ( (len f) - j = k & (k - 1) + 1 = k & j >= 1 ) by A27, A28, FINSEQ_3:27;
then ( k + 1 >= 1 & k + 1 <= i ) by A10, A28, NAT_1:11, XREAL_1:8;
then ((len f) - j) + 1 in Seg i by A28, A29;
then consider o being Element of NAT , b being adjective of T, u being type of T such that
A31: ( f . (((len f) - j) + 1) = b & ((len f) - j) + 1 = o & b ast u = p . o & u = p . (o + 1) & b is_properly_applicable_to u ) by A9;
( i + 1 = (k + 1) + j & (i + 1) - (o + 1) = ((i + 1) - o) - 1 ) by A10, A28;
then ( (i + 1) - (o + 1) = j - 1 & o + 1 >= 1 & o + 1 <= len p ) by A3, A30, A31, NAT_1:11, XREAL_1:8;
then A32: ( ((len (apply (Rev f),t2)) - (o + 1)) + 1 = j & o + 1 in dom p ) by A10, FINSEQ_3:27;
a = b by A27, A31, FINSEQ_5:def 3;
hence a is_properly_applicable_to s by A25, A27, A31, A32, FINSEQ_5:def 3; :: thesis:

end;

A33: rng (Rev f) = A by FINSEQ_5:60;
thus A is_properly_applicable_to t2 :: thesis:

proof

take Rev f ; :: according to ABCMIZ_0:def 29 :: thesis:
thus ( rng (Rev f) = A & Rev f is_properly_applicable_to t2 ) by A26, FINSEQ_5:60; :: thesis:

end;

A ast t2 = (Rev f) ast t2 by A26, A33, Th57, Th58
.= (apply (Rev f),t2) . ((len (Rev f)) + 1) ;
hence t1 = A ast t2 by A1, A10, A24, FINSEQ_5:65; :: thesis: