let T be reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TAS-structure ; for t being type of T
for A being Subset of the adjectives of T st A is_properly_applicable_to t holds
ex s being one-to-one FinSequence of the adjectives of T st
( rng s = A & s is_properly_applicable_to t )
let t be type of T; for A being Subset of the adjectives of T st A is_properly_applicable_to t holds
ex s being one-to-one FinSequence of the adjectives of T st
( rng s = A & s is_properly_applicable_to t )
let A be Subset of the adjectives of T; ( A is_properly_applicable_to t implies ex s being one-to-one FinSequence of the adjectives of T st
( rng s = A & s is_properly_applicable_to t ) )
given s9 being FinSequence of the adjectives of T such that A1:
rng s9 = A
and
A2:
s9 is_properly_applicable_to t
; ABCMIZ_0:def 29 ex s being one-to-one FinSequence of the adjectives of T st
( rng s = A & s is_properly_applicable_to t )
defpred S1[ Nat] means ex s being FinSequence of the adjectives of T st
( $1 = len s & rng s = A & s is_properly_applicable_to t );
len s9 = len s9
;
then A3:
ex k being Nat st S1[k]
by A1, A2;
consider k being Nat such that
A4:
S1[k]
and
A5:
for n being Nat st S1[n] holds
k <= n
from NAT_1:sch 5(A3);
consider s being FinSequence of the adjectives of T such that
A6:
k = len s
and
A7:
rng s = A
and
A8:
s is_properly_applicable_to t
by A4;
s is one-to-one
proof
let x,
y be
object ;
FUNCT_1:def 4 ( not x in dom s or not y in dom s or not s . x = s . y or x = y )
assume that A9:
x in dom s
and A10:
y in dom s
and A11:
s . x = s . y
and A12:
x <> y
;
contradiction
reconsider x =
x,
y =
y as
Element of
NAT by A9, A10;
(
x < y or
x > y )
by A12, XXREAL_0:1;
then consider x,
y being
Element of
NAT such that A13:
x in dom s
and A14:
y in dom s
and A15:
x < y
and A16:
s . x = s . y
by A9, A10, A11;
A17:
x >= 1
by A13, FINSEQ_3:25;
y >= 1
by A14, FINSEQ_3:25;
then consider i being
Nat such that A18:
y = 1
+ i
by 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;
A19:
y <= len s
by A14, FINSEQ_3:25;
then
i <= len s
by A18, NAT_1:13;
then A20:
len s1 = i
by FINSEQ_1:17;
x <= i
by A15, A18, NAT_1:13;
then A21:
x in dom s1
by A20, A17, FINSEQ_3:25;
s1 c= s
by TREES_1:def 1;
then consider s2 being
FinSequence such that A22:
s = s1 ^ s2
by TREES_1:1;
reconsider s2 =
s2 as
FinSequence of the
adjectives of
T by A22, FINSEQ_1:36;
A23:
len s = (len s1) + (len s2)
by A22, FINSEQ_1:22;
then A24:
len s2 >= 1
by A18, A19, A20, XREAL_1:6;
then A25:
1
in dom s2
by FINSEQ_3:25;
reconsider s21 =
s2 | (Seg 1) as
FinSequence of the
adjectives of
T by FINSEQ_1:18;
s21 c= s2
by TREES_1:def 1;
then consider s22 being
FinSequence such that A26:
s2 = s21 ^ s22
by TREES_1:1;
reconsider s22 =
s22 as
FinSequence of the
adjectives of
T by A26, FINSEQ_1:36;
A27:
len s21 = 1
by A24, FINSEQ_1:17;
then A28:
s21 = <*(s21 . 1)*>
by FINSEQ_1:40;
then A29:
rng s21 = {(s21 . 1)}
by FINSEQ_1:39;
then reconsider a =
s21 . 1 as
adjective of
T by ZFMISC_1:31;
A30:
rng s2 = (rng s21) \/ (rng s22)
by A26, FINSEQ_1:31;
a =
s2 . 1
by A28, A26, FINSEQ_1:41
.=
s . y
by A18, A22, A20, A25, FINSEQ_1:def 7
;
then
a = s1 . x
by A16, A22, A21, FINSEQ_1:def 7;
then A31:
a in rng s1
by A21, FUNCT_1:3;
then
rng s21 c= rng s1
by A29, ZFMISC_1:31;
then
(rng s1) \/ (rng s21) = rng s1
by XBOOLE_1:12;
then A32:
rng (s1 ^ s22) = ((rng s1) \/ (rng s21)) \/ (rng s22)
by FINSEQ_1:31;
A33:
s2 is_properly_applicable_to s1 ast t
by A8, A22, Th60;
A34:
s1 is_properly_applicable_to t
by A8, A22, A23, Th60;
then
rng s1 c= adjs (s1 ast t)
by Th44, Th57;
then s1 ast t =
a ast (s1 ast t)
by A31, Th24
.=
s21 ast (s1 ast t)
by A28, Th31
;
then
s22 is_properly_applicable_to s1 ast t
by A26, A33, Th60;
then A35:
s1 ^ s22 is_properly_applicable_to t
by A34, Th61;
A36:
len s2 = (len s21) + (len s22)
by A26, FINSEQ_1:22;
rng s = (rng s1) \/ (rng s2)
by A22, FINSEQ_1:31;
then
k <= len (s1 ^ s22)
by A5, A7, A35, A32, A30, XBOOLE_1:4;
then
k <= (len s1) + (len s22)
by FINSEQ_1:22;
then
(len s21) + (len s22) <= 0 + (len s22)
by A6, A23, A36, XREAL_1:6;
hence
contradiction
by A27, XREAL_1:6;
verum
end;
hence
ex s being one-to-one FinSequence of the adjectives of T st
( rng s = A & s is_properly_applicable_to t )
by A7, A8; verum