let T be reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TAS-structure ; :: thesis: for t being type of T
for A being finite Subset of the adjectives of T st ( for C being Subset of the adjectives of T st C c= A & C is_properly_applicable_to t & A ast t = C ast t holds
C = A ) holds
for s being one-to-one FinSequence of the adjectives of T st rng s = A & s is_properly_applicable_to t holds
Rev (apply (s,t)) is RedSequence of T @-->
let t be type of T; :: thesis: for A being finite Subset of the adjectives of T st ( for C being Subset of the adjectives of T st C c= A & C is_properly_applicable_to t & A ast t = C ast t holds
C = A ) holds
for s being one-to-one FinSequence of the adjectives of T st rng s = A & s is_properly_applicable_to t holds
Rev (apply (s,t)) is RedSequence of T @-->
let A be finite Subset of the adjectives of T; :: thesis: ( ( for C being Subset of the adjectives of T st C c= A & C is_properly_applicable_to t & A ast t = C ast t holds
C = A ) implies for s being one-to-one FinSequence of the adjectives of T st rng s = A & s is_properly_applicable_to t holds
Rev (apply (s,t)) is RedSequence of T @--> )
assume A1: for C being Subset of the adjectives of T st C c= A & C is_properly_applicable_to t & A ast t = C ast t holds
C = A ; :: thesis: for s being one-to-one FinSequence of the adjectives of T st rng s = A & s is_properly_applicable_to t holds
Rev (apply (s,t)) is RedSequence of T @-->
let s be one-to-one FinSequence of the adjectives of T; :: thesis: ( rng s = A & s is_properly_applicable_to t implies Rev (apply (s,t)) is RedSequence of T @--> )
assume that
A2: rng s = A and
A3: s is_properly_applicable_to t ; :: thesis: Rev (apply (s,t)) is RedSequence of T @-->
A4: len (Rev (apply (s,t))) = len (apply (s,t)) by FINSEQ_5:def 3;
hence len (Rev (apply (s,t))) > 0 ; :: according to REWRITE1:def 2 :: thesis: for b₁ being set holds
( not b₁ in dom (Rev (apply (s,t))) or not b₁ + 1 in dom (Rev (apply (s,t))) or [((Rev (apply (s,t))) . b₁),((Rev (apply (s,t))) . (b₁ + 1))] in T @--> )
let i be Nat; :: thesis: ( not i in dom (Rev (apply (s,t))) or not i + 1 in dom (Rev (apply (s,t))) or [((Rev (apply (s,t))) . i),((Rev (apply (s,t))) . (i + 1))] in T @--> )
assume that
A5: i in dom (Rev (apply (s,t))) and
A6: i + 1 in dom (Rev (apply (s,t))) ; :: thesis: [((Rev (apply (s,t))) . i),((Rev (apply (s,t))) . (i + 1))] in T @-->
A7: len (apply (s,t)) = (len s) + 1 by Def19;
then A8: (Rev (apply (s,t))) . i = (apply (s,t)) . ((((len s) + 1) - i) + 1) by A5, FINSEQ_5:def 3;
i + 1 <= (len s) + 1 by A4, A7, A6, FINSEQ_3:25;
then consider j being Nat such that
A9: (len s) + 1 = (i + 1) + j by NAT_1:10;
A10: (Rev (apply (s,t))) . (i + 1) = (apply (s,t)) . ((((len s) + 1) - (i + 1)) + 1) by A7, A6, FINSEQ_5:def 3;
A11: i >= 1 by A5, FINSEQ_3:25;
len s = i + j by A9;
then A12: j + 1 <= len s by A11, XREAL_1:6;
j + 1 >= 1 by NAT_1:11;
hence [((Rev (apply (s,t))) . i),((Rev (apply (s,t))) . (i + 1))] in T @--> by A1, A2, A3, A8, A10, A9, A12, Th70; :: thesis: verum