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 A2: ( rng s = A & s is_properly_applicable_to t ) ; :: thesis: Rev (apply s,t) is RedSequence of T @-->
A3: ( len (Rev (apply s,t)) = len (apply s,t) & len (apply s,t) = (len s) + 1 & dom (Rev (apply s,t)) = dom (apply s,t) ) by Def19, FINSEQ_5:60, FINSEQ_5:def 3;
hence len (Rev (apply s,t)) > 0 ; :: according to REWRITE1:def 2 :: thesis: for b₁ being Element of NAT 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 Element of 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 ( i in dom (Rev (apply s,t)) & i + 1 in dom (Rev (apply s,t)) ) ; :: thesis: [((Rev (apply s,t)) . i),((Rev (apply s,t)) . (i + 1))] in T @-->
then A4: ( i >= 1 & i + 1 <= (len s) + 1 & (Rev (apply s,t)) . i = (apply s,t) . ((((len s) + 1) - i) + 1) & (Rev (apply s,t)) . (i + 1) = (apply s,t) . ((((len s) + 1) - (i + 1)) + 1) ) by A3, FINSEQ_3:27, FINSEQ_5:def 3;
then consider j being Nat such that
A5: (len s) + 1 = (i + 1) + j by NAT_1:10;
( ((len s) + 1) - (i + 1) = j & ((len s) + 1) - i = j + 1 & len s = i + j ) by A5;
then ( j + 1 >= 1 & j + 1 <= len s ) by A4, NAT_1:11, XREAL_1:8;
hence [((Rev (apply s,t)) . i),((Rev (apply s,t)) . (i + 1))] in T @--> by A1, A2, A4, A5, Th71; :: thesis: verum