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 ( 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
for i being Nat st 1 <= i & i <= len s holds
[((apply (s,t)) . (i + 1)),((apply (s,t)) . i)] in T @-->
let t be 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
for i being Nat st 1 <= i & i <= len s holds
[((apply (s,t)) . (i + 1)),((apply (s,t)) . i)] in T @-->
let A be finite Subset of the adjectives of T; ( ( 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
for i being Nat st 1 <= i & i <= len s holds
[((apply (s,t)) . (i + 1)),((apply (s,t)) . i)] in 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
; for s being one-to-one FinSequence of the adjectives of T st rng s = A & s is_properly_applicable_to t holds
for i being Nat st 1 <= i & i <= len s holds
[((apply (s,t)) . (i + 1)),((apply (s,t)) . i)] in T @-->
let s be one-to-one FinSequence of the adjectives of T; ( rng s = A & s is_properly_applicable_to t implies for i being Nat st 1 <= i & i <= len s holds
[((apply (s,t)) . (i + 1)),((apply (s,t)) . i)] in T @--> )
assume that
A2:
rng s = A
and
A3:
s is_properly_applicable_to t
; for i being Nat st 1 <= i & i <= len s holds
[((apply (s,t)) . (i + 1)),((apply (s,t)) . i)] in T @-->
let j be Nat; ( 1 <= j & j <= len s implies [((apply (s,t)) . (j + 1)),((apply (s,t)) . j)] in T @--> )
assume that
A4:
1 <= j
and
A5:
j <= len s
; [((apply (s,t)) . (j + 1)),((apply (s,t)) . j)] in T @-->
A6:
len (apply (s,t)) = (len s) + 1
by Def19;
j < (len s) + 1
by A5, NAT_1:13;
then
j in dom (apply (s,t))
by A6, A4, FINSEQ_3:25;
then
(apply (s,t)) . j in rng (apply (s,t))
by FUNCT_1:3;
then reconsider tt = (apply (s,t)) . j as type of T ;
A7:
j in dom s
by A4, A5, FINSEQ_3:25;
then
s . j in rng s
by FUNCT_1:3;
then reconsider a = s . j as adjective of T ;
A8:
(apply (s,t)) . (j + 1) = a ast tt
by A7, Def19;
A9:
not a in adjs tt
proof
assume A10:
a in adjs tt
;
contradiction
consider i being
Nat such that A11:
j = 1
+ i
by A4, NAT_1:10;
reconsider i =
i as
Element of
NAT by ORDINAL1:def 12;
reconsider s1 =
s | (Seg i) as
FinSequence of the
adjectives of
T by FINSEQ_1:18;
s1 c= s
by TREES_1:def 1;
then consider s2 being
FinSequence such that A12:
s = s1 ^ s2
by TREES_1:1;
reconsider s2 =
s2 as
FinSequence of the
adjectives of
T by A12, FINSEQ_1:36;
A13:
len s = (len s1) + (len s2)
by A12, FINSEQ_1:22;
then A14:
s1 is_properly_applicable_to t
by A3, A12, Th60;
reconsider s21 =
s2 | (Seg 1) as
FinSequence of the
adjectives of
T by FINSEQ_1:18;
i <= len s
by A5, A11, NAT_1:13;
then A15:
len s1 = i
by FINSEQ_1:17;
then A16:
len s2 >= 1
by A5, A11, A13, XREAL_1:6;
then A17:
len s21 = 1
by FINSEQ_1:17;
then A18:
s21 = <*(s21 . 1)*>
by FINSEQ_1:40;
then A19:
rng s21 = {(s21 . 1)}
by FINSEQ_1:39;
then reconsider b =
s21 . 1 as
adjective of
T by ZFMISC_1:31;
A20:
1
in dom s2
by A16, FINSEQ_3:25;
s21 c= s2
by TREES_1:def 1;
then consider s22 being
FinSequence such that A21:
s2 = s21 ^ s22
by TREES_1:1;
reconsider s22 =
s22 as
FinSequence of the
adjectives of
T by A21, FINSEQ_1:36;
A22:
rng s2 = (rng s21) \/ (rng s22)
by A21, FINSEQ_1:31;
then A23:
rng s22 c= rng s2
by XBOOLE_1:7;
A24:
b =
s2 . 1
by A18, A21, FINSEQ_1:41
.=
a
by A11, A12, A15, A20, FINSEQ_1:def 7
;
then
a in rng s21
by A19, TARSKI:def 1;
then A25:
a in rng s2
by A22, XBOOLE_0:def 3;
s1 ast t = tt
by A11, A12, A13, A15, Th36;
then A26:
s1 ast t =
a ast (s1 ast t)
by A10, Th24
.=
s21 ast (s1 ast t)
by A18, A24, Th31
;
s2 is_properly_applicable_to s1 ast t
by A3, A12, Th60;
then
s22 is_properly_applicable_to s1 ast t
by A21, A26, Th60;
then A27:
s1 ^ s22 is_properly_applicable_to t
by A14, Th61;
reconsider B =
rng (s1 ^ s22) as
Subset of the
adjectives of
T ;
A28:
B = (rng s1) \/ (rng s22)
by FINSEQ_1:31;
A29:
A = (rng s1) \/ (rng s2)
by A2, A12, FINSEQ_1:31;
s ast t =
s2 ast (s1 ast t)
by A12, Th37
.=
s22 ast (s1 ast t)
by A21, A26, Th37
.=
(s1 ^ s22) ast t
by Th37
;
then A30:
A ast t =
(s1 ^ s22) ast t
by A2, A3, Th56, Th57
.=
B ast t
by A27, Th56, Th57
;
B is_properly_applicable_to t
by A27;
then
B = A
by A1, A30, A28, A29, A23, XBOOLE_1:9;
then A31:
a in B
by A29, A25, XBOOLE_0:def 3;
per cases
( a in rng s1 or a in rng s22 )
by A28, A31, XBOOLE_0:def 3;
suppose
a in rng s1
;
contradictionthen consider x being
object such that A32:
x in dom s1
and A33:
a = s1 . x
by FUNCT_1:def 3;
reconsider x =
x as
Element of
NAT by A32;
x <= len s1
by A32, FINSEQ_3:25;
then A34:
x < j
by A11, A15, NAT_1:13;
A35:
dom s1 c= dom s
by A12, FINSEQ_1:26;
s . x = a
by A12, A32, A33, FINSEQ_1:def 7;
hence
contradiction
by A7, A32, A35, A34, FUNCT_1:def 4;
verum end; suppose
a in rng s22
;
contradictionthen consider x being
object such that A36:
x in dom s22
and A37:
a = s22 . x
by FUNCT_1:def 3;
reconsider x =
x as
Element of
NAT by A36;
A38:
1
+ x in dom s2
by A17, A21, A36, FINSEQ_1:28;
x >= 0 + 1
by A36, FINSEQ_3:25;
then A39:
j + x > j + 0
by XREAL_1:6;
s2 . (1 + x) = a
by A17, A21, A36, A37, FINSEQ_1:def 7;
then A40:
s . (i + (1 + x)) = a
by A12, A15, A38, FINSEQ_1:def 7;
i + (1 + x) in dom s
by A12, A15, A38, FINSEQ_1:28;
hence
contradiction
by A7, A11, A39, A40, FUNCT_1:def 4;
verum end;
end;
a is_properly_applicable_to tt
by A3, A7;
hence
[((apply (s,t)) . (j + 1)),((apply (s,t)) . j)] in T @-->
by A8, A9, Def31; verum