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 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; :: thesis: 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; :: thesis: ( 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 s' being FinSequence of the adjectives of T such that A1:
( rng s' = A & s' is_properly_applicable_to t )
; :: according to ABCMIZ_0:def 29 :: thesis: 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 s' = len s'
;
then A2:
ex k being Nat st S1[k]
by A1;
consider k being Nat such that
A3:
S1[k]
and
A4:
for n being Nat st S1[n] holds
k <= n
from NAT_1:sch 5(A2);
consider s being FinSequence of the adjectives of T such that
A5:
( k = len s & rng s = A & s is_properly_applicable_to t )
by A3;
s is one-to-one
proof
let x,
y be
set ;
:: according to FUNCT_1:def 8 :: thesis: ( not x in dom s or not y in dom s or not s . x = s . y or x = y )
assume A6:
(
x in dom s &
y in dom s &
s . x = s . y &
x <> y )
;
:: thesis: contradiction
then reconsider x =
x,
y =
y as
Element of
NAT ;
(
x < y or
x > y )
by A6, XXREAL_0:1;
then consider x,
y being
Element of
NAT such that A7:
(
x in dom s &
y in dom s &
x < y &
s . x = s . y )
by A6;
y >= 1
by A7, FINSEQ_3:27;
then consider i being
Nat such that A8:
y = 1
+ i
by NAT_1:10;
reconsider i =
i as
Element of
NAT by ORDINAL1:def 13;
reconsider s1 =
s | (Seg i) as
FinSequence of the
adjectives of
T by FINSEQ_1:23;
s1 c= s
by TREES_1:def 1;
then consider s2 being
FinSequence such that A9:
s = s1 ^ s2
by TREES_1:8;
reconsider s2 =
s2 as
FinSequence of the
adjectives of
T by A9, FINSEQ_1:50;
reconsider s21 =
s2 | (Seg 1) as
FinSequence of the
adjectives of
T by FINSEQ_1:23;
A10:
(
y <= len s &
i < y )
by A7, A8, FINSEQ_3:27, NAT_1:13;
then
i <= len s
by XXREAL_0:2;
then A11:
(
len s = (len s1) + (len s2) &
len s1 = i )
by A9, FINSEQ_1:21, FINSEQ_1:35;
then A12:
len s2 >= 1
by A8, A10, XREAL_1:8;
then A13:
len s21 = 1
by FINSEQ_1:21;
then A14:
s21 = <*(s21 . 1)*>
by FINSEQ_1:57;
then A15:
rng s21 = {(s21 . 1)}
by FINSEQ_1:56;
then reconsider a =
s21 . 1 as
adjective of
T by ZFMISC_1:37;
s21 c= s2
by TREES_1:def 1;
then consider s22 being
FinSequence such that A16:
s2 = s21 ^ s22
by TREES_1:8;
reconsider s22 =
s22 as
FinSequence of the
adjectives of
T by A16, FINSEQ_1:50;
A17:
1
in dom s2
by A12, FINSEQ_3:27;
A18:
a =
s2 . 1
by A14, A16, FINSEQ_1:58
.=
s . y
by A8, A9, A11, A17, FINSEQ_1:def 7
;
(
x <= i &
x >= 1 )
by A7, A8, FINSEQ_3:27, NAT_1:13;
then A19:
(
x in dom s1 &
s1 is_properly_applicable_to t )
by A5, A9, A11, Th61, FINSEQ_3:27;
then
(
a = s1 . x &
s1 is_applicable_to t )
by A7, A9, A18, Th58, FINSEQ_1:def 7;
then A20:
(
a in rng s1 &
rng s1 c= adjs (s1 ast t) )
by A19, Th45, FUNCT_1:12;
then A21:
s1 ast t =
a ast (s1 ast t)
by Th25
.=
s21 ast (s1 ast t)
by A14, Th32
;
s2 is_properly_applicable_to s1 ast t
by A5, A9, Th61;
then
s22 is_properly_applicable_to s1 ast t
by A16, A21, Th61;
then A22:
s1 ^ s22 is_properly_applicable_to t
by A19, Th62;
rng s21 c= rng s1
by A15, A20, ZFMISC_1:37;
then
(rng s1) \/ (rng s21) = rng s1
by XBOOLE_1:12;
then
(
rng (s1 ^ s22) = ((rng s1) \/ (rng s21)) \/ (rng s22) &
rng s = (rng s1) \/ (rng s2) &
rng s2 = (rng s21) \/ (rng s22) )
by A9, A16, FINSEQ_1:44;
then
k <= len (s1 ^ s22)
by A4, A5, A22, XBOOLE_1:4;
then
(
k <= (len s1) + (len s22) &
len s2 = (len s21) + (len s22) )
by A16, FINSEQ_1:35;
then
(len s21) + (len s22) <= 0 + (len s22)
by A5, A11, XREAL_1:8;
hence
contradiction
by A13, XREAL_1:8;
:: thesis: 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 A5; :: thesis: verum