let T be reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TAS-structure ; for t being type of T
for A being finite Subset of the adjectives of T st A is_properly_applicable_to t holds
T @--> reduces A ast t,t
set R = T @--> ;
let t be type of T; for A being finite Subset of the adjectives of T st A is_properly_applicable_to t holds
T @--> reduces A ast t,t
let A be finite Subset of the adjectives of T; ( A is_properly_applicable_to t implies T @--> reduces A ast t,t )
assume
A is_properly_applicable_to t
; T @--> reduces A ast t,t
then consider A9 being Subset of the adjectives of T such that
A9 c= A
and
A1:
A9 is_properly_applicable_to t
and
A2:
A ast t = A9 ast t
and
A3:
for C being Subset of the adjectives of T st C c= A9 & C is_properly_applicable_to t & A ast t = C ast t holds
C = A9
by Th64;
consider s being one-to-one FinSequence of the adjectives of T such that
A4:
rng s = A9
and
A5:
s is_properly_applicable_to t
by A1, Th65;
reconsider p = Rev (apply (s,t)) as RedSequence of T @--> by A2, A3, A4, A5, Th71;
take
p
; REWRITE1:def 3 ( p . 1 = A ast t & p . (len p) = t )
thus p . 1 =
(apply (s,t)) . (len (apply (s,t)))
by FINSEQ_5:62
.=
s ast t
by Def19
.=
A ast t
by A2, A4, A5, Th56, Th57
; p . (len p) = t
thus p . (len p) =
p . (len (apply (s,t)))
by FINSEQ_5:def 3
.=
(apply (s,t)) . 1
by FINSEQ_5:62
.=
t
by Def19
; verum