let T be reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TAS-structure ; :: thesis: for t1, t2 being type of T st T @--> reduces t1,t2 holds
ex A being finite Subset of the adjectives of T st
( A is_properly_applicable_to t2 & t1 = A ast t2 )
let t1, t2 be type of T; :: thesis: ( T @--> reduces t1,t2 implies ex A being finite Subset of the adjectives of T st
( A is_properly_applicable_to t2 & t1 = A ast t2 ) )
set R = T @--> ;
given p being RedSequence of T @--> such that A1: p . 1 = t1 and
A2: t2 = p . (len p) ; :: according to REWRITE1:def 3 :: thesis: ex A being finite Subset of the adjectives of T st
( A is_properly_applicable_to t2 & t1 = A ast t2 )
defpred S₁[ object , object ] 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 );
A3: len (Rev p) = len p by FINSEQ_5:def 3;
A4: ((len p) - 1) + 1 = len p ;
A5: len p >= 0 + 1 by NAT_1:13;
then consider i being Nat such that
A6: len p = 1 + i by NAT_1:10;
reconsider i = i as Element of NAT by ORDINAL1:def 12;

A7: now :: thesis: for x being object st x in Seg i holds
ex y being object st
( y in the adjectives of T & S₁[x,y] )

let x be object ; :: thesis: ( x in Seg i implies ex y being object st
( y in the adjectives of T & S₁[x,y] ) )
assume A8: x in Seg i ; :: thesis: ex y being object st
( y in the adjectives of T & S₁[x,y] )
then reconsider j = x as Element of NAT ;
A9: j >= 1 by A8, FINSEQ_1:1;
then A10: 1 <= j + 1 by NAT_1:13;
A11: j <= i by A8, FINSEQ_1:1;
then j < len p by A6, NAT_1:13;
then A12: j in dom p by A9, FINSEQ_3:25;
j + 1 <= len p by A6, A11, XREAL_1:6;
then j + 1 in dom p by A10, FINSEQ_3:25;
then A13: [(p . j),(p . (j + 1))] in T @--> by A12, REWRITE1:def 2;
then reconsider q1 = p . j, q2 = p . (j + 1) as type of T by ZFMISC_1:87;
ex a being adjective of T st
( not a in adjs q2 & a is_properly_applicable_to q2 & a ast q2 = q1 ) by A13, Def31;
hence ex y being object st
( y in the adjectives of T & S₁[x,y] ) ; :: thesis: verum

end;

consider f being Function such that
A14: ( dom f = Seg i & rng f c= the adjectives of T ) and
A15: for x being object st x in Seg i holds
S₁[x,f . x] from FUNCT_1:sch 6(A7);
f is FinSequence by A14, FINSEQ_1:def 2;
then reconsider f = f as FinSequence of the adjectives of T by A14, FINSEQ_1:def 4;
A16: len f = i by A14, FINSEQ_1:def 3;
set r = Rev f;
defpred S₂[ Nat] means ( 1 + $1 <= len p implies (Rev p) . (1 + $1) = (apply ((Rev f),t2)) . (1 + $1) );
A17: len (Rev f) = len f by FINSEQ_5:def 3;

A18: now :: thesis: for j being Nat st S₂[j] holds
S₂[j + 1]

let j be Nat; :: thesis: ( S₂[j] implies S₂[j + 1] )
assume A19: S₂[j] ; :: thesis: S₂[j + 1]

now :: thesis: ( 1 + (j + 1) <= len p implies (Rev p) . (1 + (j + 1)) = (apply ((Rev f),t2)) . (1 + (j + 1)) )

A20: j + 1 >= 1 by NAT_1:11;
assume A21: 1 + (j + 1) <= len p ; :: thesis: (Rev p) . (1 + (j + 1)) = (apply ((Rev f),t2)) . (1 + (j + 1))
then j + 1 <= i by A6, XREAL_1:6;
then consider x being Nat such that
A22: i = (j + 1) + x by NAT_1:10;
reconsider x = x as Element of NAT by ORDINAL1:def 12;
A23: (i + 1) - (j + 1) = x + 1 by A22;
j + 1 < len p by A21, NAT_1:13;
then j + 1 in dom (Rev p) by A3, A20, FINSEQ_3:25;
then A24: (Rev p) . (j + 1) = p . ((x + 1) + 1) by A6, A23, FINSEQ_5:def 3;
A25: (i + 1) - (1 + (j + 1)) = x by A22;
1 + (j + 1) >= 1 by NAT_1:11;
then 1 + (j + 1) in dom (Rev p) by A3, A21, FINSEQ_3:25;
then A26: (Rev p) . (1 + (j + 1)) = p . (x + 1) by A6, A25, FINSEQ_5:def 3;
i = (x + 1) + j by A22;
then A27: i >= x + 1 by NAT_1:11;
x + 1 >= 1 by NAT_1:11;
then x + 1 in Seg i by A27;
then consider k being Element of NAT , a being adjective of T, t being type of T such that
A28: f . (x + 1) = a and
A29: x + 1 = k and
A30: a ast t = p . k and
A31: t = p . (k + 1) and
a is_properly_applicable_to t by A15;
A32: j + 1 >= 1 by NAT_1:11;
j + 1 <= i by A22, NAT_1:11;
then A33: j + 1 in dom (Rev f) by A17, A16, A32, FINSEQ_3:25;
then (Rev f) . (j + 1) = f . (((len f) - (j + 1)) + 1) by FINSEQ_5:def 3
.= a by A16, A22, A28 ;
hence (Rev p) . (1 + (j + 1)) = (apply ((Rev f),t2)) . (1 + (j + 1)) by A19, A21, A29, A30, A31, A33, A24, A26, Def19, NAT_1:13; :: thesis: verum

end;

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

end;

reconsider A = rng f as finite Subset of the adjectives of T ;
take A ; :: thesis: ( A is_properly_applicable_to t2 & t1 = A ast t2 )
A34: len (apply ((Rev f),t2)) = (len (Rev f)) + 1 by Def19;
1 in dom (Rev p) by A5, A3, FINSEQ_3:25;
then (Rev p) . 1 = t2 by A2, A4, FINSEQ_5:def 3;
then A35: S₂[ 0 ] by Def19;
A36: for j being Nat holds S₂[j] from NAT_1:sch 2(A35, A18);

now :: thesis: for j being Nat st 1 <= j & j <= len p holds
(Rev p) . j = (apply ((Rev f),t2)) . j

let j be Nat; :: thesis: ( 1 <= j & j <= len p implies (Rev p) . j = (apply ((Rev f),t2)) . j )
assume 1 <= j ; :: thesis: ( j <= len p implies (Rev p) . j = (apply ((Rev f),t2)) . j )
then consider k being Nat such that
A37: j = 1 + k by NAT_1:10;
thus ( j <= len p implies (Rev p) . j = (apply ((Rev f),t2)) . j ) by A36, A37; :: thesis: verum

end;

then A38: Rev p = apply ((Rev f),t2) by A6, A17, A34, A16, A3;
then A39: p = Rev (apply ((Rev f),t2)) ;
A40: Rev f is_properly_applicable_to t2

proof

let j be Nat; :: according to ABCMIZ_0:def 28 :: thesis: for a being adjective of T
for s being type of T st j in dom (Rev f) & a = (Rev f) . j & s = (apply ((Rev f),t2)) . j holds
a is_properly_applicable_to s
let a be adjective of T; :: thesis: for s being type of T st j in dom (Rev f) & a = (Rev f) . j & s = (apply ((Rev f),t2)) . j holds
a is_properly_applicable_to s
let s be type of T; :: thesis: ( j in dom (Rev f) & a = (Rev f) . j & s = (apply ((Rev f),t2)) . j implies a is_properly_applicable_to s )
assume that
A41: j in dom (Rev f) and
A42: a = (Rev f) . j and
A43: s = (apply ((Rev f),t2)) . j ; :: thesis: a is_properly_applicable_to s
j <= len (Rev f) by A41, FINSEQ_3:25;
then consider k being Nat such that
A44: len (Rev f) = j + k by NAT_1:10;
A45: len (Rev f) = len f by FINSEQ_5:def 3;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
A46: k + 1 >= 1 by NAT_1:11;
A47: j >= 1 by A41, FINSEQ_3:25;
then k + 1 <= i by A16, A44, A45, XREAL_1:6;
then ((len f) - j) + 1 in Seg i by A44, A45, A46;
then consider o being Element of NAT , b being adjective of T, u being type of T such that
A48: f . (((len f) - j) + 1) = b and
A49: ((len f) - j) + 1 = o and
b ast u = p . o and
A50: u = p . (o + 1) and
A51: b is_properly_applicable_to u by A15;
A52: o + 1 >= 1 by NAT_1:11;
i + 1 = (k + 1) + j by A17, A16, A44;
then o + 1 <= len p by A6, A44, A45, A47, A49, XREAL_1:6;
then A53: o + 1 in dom p by A52, FINSEQ_3:25;
A54: a = b by A41, A42, A48, FINSEQ_5:def 3;
((len (apply ((Rev f),t2))) - (o + 1)) + 1 = j by A17, A34, A49;
hence a is_properly_applicable_to s by A39, A43, A50, A51, A53, A54, FINSEQ_5:def 3; :: thesis: verum

end;

thus A is_properly_applicable_to t2 :: thesis: t1 = A ast t2

proof

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

end;

rng (Rev f) = A by FINSEQ_5:57;
then A ast t2 = (Rev f) ast t2 by A40, Th56, Th57
.= (apply ((Rev f),t2)) . ((len (Rev f)) + 1) ;
hence t1 = A ast t2 by A1, A34, A3, A38, FINSEQ_5:62; :: thesis: verum