let n be Nat; for A being affinely-independent Subset of (TOP-REAL n) st card A = n + 1 holds
ind (conv A) = n
let A be affinely-independent Subset of (TOP-REAL n); ( card A = n + 1 implies ind (conv A) = n )
set TR = TOP-REAL n;
assume A1:
card A = n + 1
; ind (conv A) = n
set C = conv A;
A2:
ind (conv A) >= n
proof
set E = the
Enumeration of
A;
assume A3:
ind (conv A) < n
;
contradiction
not
A is
empty
by A1;
then reconsider C =
conv A as non
empty Subset of
(TOP-REAL n) ;
ind C is
natural
;
then reconsider n1 =
n - 1 as
Nat by A3;
deffunc H1(
object )
-> Element of
bool the
carrier of
(TOP-REAL n) =
C \ (conv (A \ {( the Enumeration of A . $1)}));
reconsider c =
C as
Subset of
TopStruct(# the
carrier of
(TOP-REAL n), the
topology of
(TOP-REAL n) #) ;
set TRC =
(TOP-REAL n) | C;
set carr = the
carrier of
((TOP-REAL n) | C);
A4:
(
TopStruct(# the
carrier of
(TOP-REAL n), the
topology of
(TOP-REAL n) #)
= TopSpaceMetr (Euclid n) &
TopStruct(# the
carrier of
((TOP-REAL n) | C), the
topology of
((TOP-REAL n) | C) #)
= TopStruct(# the
carrier of
(TOP-REAL n), the
topology of
(TOP-REAL n) #)
| c )
by EUCLID:def 8, PRE_TOPC:36;
consider f being
FinSequence such that A5:
(
len f = len the
Enumeration of
A & ( for
k being
Nat st
k in dom f holds
f . k = H1(
k) ) )
from FINSEQ_1:sch 2();
A6:
[#] ((TOP-REAL n) | C) = C
by PRE_TOPC:def 5;
rng f c= bool the
carrier of
((TOP-REAL n) | C)
then reconsider R =
rng f as
finite Subset-Family of
((TOP-REAL n) | C) ;
A9:
rng the
Enumeration of
A = A
by RLAFFIN3:def 1;
then A10:
len the
Enumeration of
A = card A
by FINSEQ_4:62;
A11:
dom f = dom the
Enumeration of
A
by A5, FINSEQ_3:29;
the
carrier of
((TOP-REAL n) | C) c= union R
proof
let x be
object ;
TARSKI:def 3 ( not x in the carrier of ((TOP-REAL n) | C) or x in union R )
assume A12:
x in the
carrier of
((TOP-REAL n) | C)
;
x in union R
assume A13:
not
x in union R
;
contradiction
now for y being set st y in A holds
(x |-- A) . y = 0 let y be
set ;
( y in A implies (x |-- A) . y = 0 )assume A14:
y in A
;
(x |-- A) . y = 0 then consider n being
object such that A15:
n in dom the
Enumeration of
A
and A16:
the
Enumeration of
A . n = y
by A9, FUNCT_1:def 3;
reconsider n =
n as
Nat by A15;
f . n = H1(
n)
by A5, A11, A15;
then
H1(
n)
in R
by A11, A15, FUNCT_1:def 3;
then
not
x in H1(
n)
by A13, TARSKI:def 4;
then
(
conv (A \ {( the Enumeration of A . n)}) c= Affin (A \ {( the Enumeration of A . n)}) &
x in conv (A \ {( the Enumeration of A . n)}) )
by A6, A12, RLAFFIN1:65, XBOOLE_0:def 5;
then A17:
x |-- A = x |-- (A \ {( the Enumeration of A . n)})
by RLAFFIN1:77, XBOOLE_1:36;
(
Carrier (x |-- (A \ {( the Enumeration of A . n)})) c= A \ {( the Enumeration of A . n)} & the
Enumeration of
A . n in {( the Enumeration of A . n)} )
by RLVECT_2:def 6, TARSKI:def 1;
then
not the
Enumeration of
A . n in Carrier (x |-- (A \ {( the Enumeration of A . n)}))
by XBOOLE_0:def 5;
hence
(x |-- A) . y = 0
by A14, A16, A17, RLVECT_2:19;
verum end;
then A18:
x in conv (A \ A)
by A6, A12, RLAFFIN1:76;
A \ A = {}
by XBOOLE_1:37;
hence
contradiction
by A18;
verum
end;
then A19:
R is
Cover of
((TOP-REAL n) | C)
by SETFAM_1:def 11;
then A22:
(
ind ((TOP-REAL n) | C) = ind C &
R is
open )
by TOPDIM_1:17, TOPS_2:def 1;
ind C < n1 + 1
by A3;
then
ind C <= n1
by NAT_1:13;
then consider G being
finite Subset-Family of
((TOP-REAL n) | C) such that A23:
G is
open
and A24:
G is
Cover of
((TOP-REAL n) | C)
and A25:
G is_finer_than R
and
card G <= (card R) * (n1 + 1)
and A26:
order G <= n1
by A4, A22, A19, TOPDIM_2:23;
defpred S1[
Nat,
set ,
set ]
means $3
= { g where g is Subset of ((TOP-REAL n) | C) : ( g in G & ( g c= f . ($1 + 1) or g in $2 ) ) } ;
defpred S2[
set ]
means ( $1
in G & $1
c= f . 1 );
consider G0 being
Subset-Family of
((TOP-REAL n) | C) such that A27:
for
x being
set holds
(
x in G0 iff (
x in bool the
carrier of
((TOP-REAL n) | C) &
S2[
x] ) )
from SUBSET_1:sch 1();
A28:
for
k being
Nat st 1
<= k &
k < len the
Enumeration of
A holds
for
x being
Element of
bool (bool the carrier of ((TOP-REAL n) | C)) ex
y being
Element of
bool (bool the carrier of ((TOP-REAL n) | C)) st
S1[
k,
x,
y]
consider p being
FinSequence of
bool (bool the carrier of ((TOP-REAL n) | C)) such that A29:
len p = len the
Enumeration of
A
and A30:
(
p /. 1
= G0 or
len the
Enumeration of
A = 0 )
and A31:
for
k being
Nat st 1
<= k &
k < len the
Enumeration of
A holds
S1[
k,
p /. k,
p /. (k + 1)]
from NAT_2:sch 1(A28);
defpred S3[
Nat,
object ]
means ( ( $1
= 1 implies $2
= union G0 ) & ( $1
<> 1 implies $2
= union ((p . $1) \ (p . ($1 - 1))) ) );
A32:
for
k being
Nat st
k in Seg (len the Enumeration of A) holds
ex
x being
object st
S3[
k,
x]
consider h being
FinSequence such that A33:
dom h = Seg (len the Enumeration of A)
and A34:
for
k being
Nat st
k in Seg (len the Enumeration of A) holds
S3[
k,
h . k]
from FINSEQ_1:sch 1(A32);
A35:
dom p = Seg (len the Enumeration of A)
by A29, FINSEQ_1:def 3;
rng h c= bool the
carrier of
((TOP-REAL n) | C)
then reconsider h =
h as
FinSequence of
bool the
carrier of
((TOP-REAL n) | C) by FINSEQ_1:def 4;
A38:
A is non
empty affinely-independent Subset of
(TOP-REAL n)
by A1;
A39:
1
<= n + 1
by NAT_1:11;
the
carrier of
((TOP-REAL n) | C) c= union (rng h)
proof
let x be
object ;
TARSKI:def 3 ( not x in the carrier of ((TOP-REAL n) | C) or x in union (rng h) )
assume
x in the
carrier of
((TOP-REAL n) | C)
;
x in union (rng h)
then
x in union G
by A24, SETFAM_1:45;
then consider y being
set such that A40:
x in y
and A41:
y in G
by TARSKI:def 4;
consider z being
set such that A42:
z in R
and A43:
y c= z
by A25, A41, SETFAM_1:def 2;
consider k being
object such that A44:
k in dom f
and A45:
f . k = z
by A42, FUNCT_1:def 3;
reconsider k =
k as
Nat by A44;
A46:
k >= 1
by A44, FINSEQ_3:25;
A47:
len the
Enumeration of
A >= k
by A5, A44, FINSEQ_3:25;
per cases
( k = 1 or y in G0 or ( k > 1 & not y in G0 ) )
by A46, XXREAL_0:1;
suppose A48:
(
k = 1 or
y in G0 )
;
x in union (rng h)A49:
1
in Seg (len the Enumeration of A)
by A1, A10, A39, FINSEQ_1:1;
then A50:
h . 1
= union G0
by A34;
y in G0
by A27, A41, A43, A45, A48;
then A51:
x in h . 1
by A40, A50, TARSKI:def 4;
h . 1
in rng h
by A33, A49, FUNCT_1:def 3;
hence
x in union (rng h)
by A51, TARSKI:def 4;
verum end; suppose A52:
(
k > 1 & not
y in G0 )
;
x in union (rng h)defpred S4[
Nat]
means ( $1
> 1 & $1
<= len the
Enumeration of
A &
y c= f . $1 );
A53:
ex
k being
Nat st
S4[
k]
by A43, A45, A47, A52;
consider m being
Nat such that A54:
(
S4[
m] & ( for
n being
Nat st
S4[
n] holds
m <= n ) )
from NAT_1:sch 5(A53);
reconsider m1 =
m - 1 as
Element of
NAT by A54, NAT_1:20;
defpred S5[
Nat]
means ( 1
<= $1 & $1
<= m1 implies not
y in p /. $1 );
m1 + 1
<= len the
Enumeration of
A
by A54;
then A55:
m1 < len the
Enumeration of
A
by NAT_1:13;
A56:
for
n being
Nat st
S5[
n] holds
S5[
n + 1]
A62:
S5[
0 ]
;
A63:
for
n being
Nat holds
S5[
n]
from NAT_1:sch 2(A62, A56);
A64:
m in dom p
by A29, A54, FINSEQ_3:25;
then A65:
h . m in rng h
by A35, A33, FUNCT_1:def 3;
m1 + 1
> 1
by A54;
then A66:
m1 >= 1
by NAT_1:13;
then A67:
p /. m = { g where g is Subset of ((TOP-REAL n) | C) : ( g in G & ( g c= f . (m1 + 1) or g in p /. m1 ) ) }
by A31, A55;
m1 in dom p
by A29, A66, A55, FINSEQ_3:25;
then
p . m1 = p /. m1
by PARTFUN1:def 6;
then A68:
not
y in p . m1
by A66, A63;
p . m = p /. m
by A64, PARTFUN1:def 6;
then
y in p . m
by A41, A54, A67;
then
y in (p . m) \ (p . m1)
by A68, XBOOLE_0:def 5;
then A69:
x in union ((p . m) \ (p . m1))
by A40, TARSKI:def 4;
h . m = union ((p . m) \ (p . m1))
by A35, A34, A54, A64;
hence
x in union (rng h)
by A69, A65, TARSKI:def 4;
verum end;
end;
then A70:
rng h is
Cover of
((TOP-REAL n) | C)
by SETFAM_1:def 11;
now for A being Subset of ((TOP-REAL n) | C) st A in rng h holds
A is open let A be
Subset of
((TOP-REAL n) | C);
( A in rng h implies b1 is open )assume
A in rng h
;
b1 is open then consider k being
object such that A71:
k in dom h
and A72:
h . k = A
by FUNCT_1:def 3;
reconsider k =
k as
Nat by A71;
A73:
k >= 1
by A33, A71, FINSEQ_1:1;
per cases
( k = 1 or k > 1 )
by A73, XXREAL_0:1;
suppose A76:
k > 1
;
b1 is open then reconsider k1 =
k - 1 as
Element of
NAT by NAT_1:20;
k1 + 1
> 1
by A76;
then A77:
k1 >= 1
by NAT_1:13;
k1 + 1
<= len the
Enumeration of
A
by A33, A71, FINSEQ_1:1;
then A78:
k1 < len the
Enumeration of
A
by NAT_1:13;
then
k1 in dom p
by A29, A77, FINSEQ_3:25;
then A79:
p . k1 = p /. k1
by PARTFUN1:def 6;
A80:
S1[
k1,
p /. k1,
p /. (k1 + 1)]
by A31, A77, A78;
p /. k c= G
then
p /. k is
open
by A23, TOPS_2:11;
then A81:
(p /. k) \ (p /. (k - 1)) is
open
by TOPS_2:15;
A82:
p . k = p /. k
by A35, A33, A71, PARTFUN1:def 6;
A = union ((p . k) \ (p . (k - 1)))
by A33, A34, A71, A72, A76;
hence
A is
open
by A82, A81, A79, TOPS_2:19;
verum end; end;
then A83:
rng h is
open
by TOPS_2:def 1;
(TOP-REAL n) | C is
compact
by COMPTS_1:3;
then consider gx being
Subset-Family of
((TOP-REAL n) | C) such that
gx is
open
and A84:
gx is
Cover of
((TOP-REAL n) | C)
and A85:
clf gx is_finer_than rng h
and A86:
gx is
locally_finite
by A4, A70, A83, PCOMPS_1:22, PCOMPS_2:3;
set cgx =
clf gx;
defpred S4[
object ,
object ]
means $2
= union { u where u is Subset of ((TOP-REAL n) | C) : ( u in clf gx & u c= h . $1 ) } ;
A87:
for
k being
Nat st
k in Seg (len the Enumeration of A) holds
ex
x being
Element of
bool the
carrier of
((TOP-REAL n) | C) st
S4[
k,
x]
consider GX being
FinSequence of
bool the
carrier of
((TOP-REAL n) | C) such that A88:
(
dom GX = Seg (len the Enumeration of A) & ( for
k being
Nat st
k in Seg (len the Enumeration of A) holds
S4[
k,
GX . k] ) )
from FINSEQ_1:sch 5(A87);
A89:
for
i being
Nat st
i in dom GX holds
GX . i c= h . i
A91:
dom the
Enumeration of
A = Seg (len the Enumeration of A)
by FINSEQ_1:def 3;
A92:
for
k being
Nat st
k in Seg (len the Enumeration of A) holds
h . k misses conv (A \ {( the Enumeration of A . k)})
proof
let k be
Nat;
( k in Seg (len the Enumeration of A) implies h . k misses conv (A \ {( the Enumeration of A . k)}) )
assume A93:
k in Seg (len the Enumeration of A)
;
h . k misses conv (A \ {( the Enumeration of A . k)})
then A94:
k >= 1
by FINSEQ_1:1;
A95:
S3[
k,
h . k]
by A34, A93;
assume
h . k meets conv (A \ {( the Enumeration of A . k)})
;
contradiction
then consider x being
object such that A96:
x in h . k
and A97:
x in conv (A \ {( the Enumeration of A . k)})
by XBOOLE_0:3;
per cases
( k = 1 or k > 1 )
by A94, XXREAL_0:1;
suppose A101:
k > 1
;
contradictionthen reconsider k1 =
k - 1 as
Element of
NAT by NAT_1:20;
len the
Enumeration of
A >= k1 + 1
by A93, FINSEQ_1:1;
then A102:
len the
Enumeration of
A > k1
by NAT_1:13;
k1 + 1
> 1
by A101;
then A103:
k1 >= 1
by NAT_1:13;
then A104:
S1[
k1,
p /. k1,
p /. (k1 + 1)]
by A31, A102;
k1 in dom p
by A29, A103, A102, FINSEQ_3:25;
then A105:
p /. k1 = p . k1
by PARTFUN1:def 6;
A106:
p /. k = p . k
by A35, A93, PARTFUN1:def 6;
consider y being
set such that A107:
x in y
and A108:
y in (p . k) \ (p . (k - 1))
by A95, A96, A101, TARSKI:def 4;
y in p . k
by A108;
then consider g being
Subset of
((TOP-REAL n) | C) such that A109:
y = g
and
g in G
and A110:
(
g c= f . k or
g in p . k1 )
by A104, A106, A105;
f . k = H1(
k)
by A5, A11, A91, A93;
hence
contradiction
by A97, A107, A108, A109, A110, XBOOLE_0:def 5;
verum end;
end;
the
carrier of
((TOP-REAL n) | C) c= union (rng GX)
proof
let x be
object ;
TARSKI:def 3 ( not x in the carrier of ((TOP-REAL n) | C) or x in union (rng GX) )
assume A111:
x in the
carrier of
((TOP-REAL n) | C)
;
x in union (rng GX)
(
union gx = the
carrier of
((TOP-REAL n) | C) &
union gx c= union (clf gx) )
by A84, PCOMPS_1:19, SETFAM_1:45;
then consider y being
set such that A112:
x in y
and A113:
y in clf gx
by A111, TARSKI:def 4;
consider r being
set such that A114:
r in rng h
and A115:
y c= r
by A85, A113, SETFAM_1:def 2;
consider k being
object such that A116:
k in dom h
and A117:
h . k = r
by A114, FUNCT_1:def 3;
A118:
S4[
k,
GX . k]
by A33, A88, A116;
A119:
GX . k in rng GX
by A33, A88, A116, FUNCT_1:def 3;
y in { u where u is Subset of ((TOP-REAL n) | C) : ( u in clf gx & u c= h . k ) }
by A113, A115, A117;
then
x in GX . k
by A112, A118, TARSKI:def 4;
hence
x in union (rng GX)
by A119, TARSKI:def 4;
verum
end;
then A120:
rng GX is
Cover of
((TOP-REAL n) | C)
by SETFAM_1:def 11;
A121:
for
S being
Subset of
(dom GX) holds
conv ( the Enumeration of A .: S) c= union (GX .: S)
proof
let S be
Subset of
(dom GX);
conv ( the Enumeration of A .: S) c= union (GX .: S)
A122:
rng GX = GX .: (dom GX)
by RELAT_1:113;
A123:
union (rng GX) = the
carrier of
((TOP-REAL n) | C)
by A120, SETFAM_1:45;
per cases
( S = dom GX or not dom GX c= S )
by XBOOLE_0:def 10;
suppose A124:
not
dom GX c= S
;
conv ( the Enumeration of A .: S) c= union (GX .: S)set U =
{ (conv (A \ {( the Enumeration of A . i)})) where i is Element of NAT : i in (dom the Enumeration of A) \ S } ;
not
(dom GX) \ S is
empty
by A124, XBOOLE_1:37;
then A125:
conv ( the Enumeration of A .: S) = meet { (conv (A \ {( the Enumeration of A . i)})) where i is Element of NAT : i in (dom the Enumeration of A) \ S }
by A91, A88, Th12;
A126:
meet { (conv (A \ {( the Enumeration of A . i)})) where i is Element of NAT : i in (dom the Enumeration of A) \ S } misses union (GX .: ((dom the Enumeration of A) \ S))
dom GX = dom the
Enumeration of
A
by A88, FINSEQ_1:def 3;
then rng GX =
GX .: (S \/ ((dom the Enumeration of A) \ S))
by A122, XBOOLE_1:45
.=
(GX .: S) \/ (GX .: ((dom the Enumeration of A) \ S))
by RELAT_1:120
;
then A135:
(union (GX .: S)) \/ (union (GX .: ((dom the Enumeration of A) \ S))) = C
by A6, A123, ZFMISC_1:78;
conv ( the Enumeration of A .: S) c= C
by A9, RELAT_1:111, RLAFFIN1:3;
hence
conv ( the Enumeration of A .: S) c= union (GX .: S)
by A125, A135, A126, XBOOLE_1:73;
verum end;
end;
A136:
clf gx is
locally_finite
by A86, PCOMPS_1:18;
then A139:
rng GX is
closed
by TOPS_2:def 2;
len GX = card A
by A10, A88, FINSEQ_1:def 3;
then
not
meet (rng GX) is
empty
by A139, A38, A121, Th22;
then consider I being
object such that A140:
I in meet (rng GX)
by XBOOLE_0:def 1;
defpred S5[
Nat,
set ]
means ( $2
in G &
I in $2 & $2
in p . $1 & ( $1
<> 1 implies not $2
in p . ($1 - 1) ) );
A141:
for
k being
Nat st
k in Seg (len the Enumeration of A) holds
ex
x being
Element of
bool the
carrier of
((TOP-REAL n) | C) st
S5[
k,
x]
proof
let k be
Nat;
( k in Seg (len the Enumeration of A) implies ex x being Element of bool the carrier of ((TOP-REAL n) | C) st S5[k,x] )
assume A142:
k in Seg (len the Enumeration of A)
;
ex x being Element of bool the carrier of ((TOP-REAL n) | C) st S5[k,x]
then A143:
k >= 1
by FINSEQ_1:1;
A144:
k <= len the
Enumeration of
A
by A142, FINSEQ_1:1;
A145:
(
GX . k c= h . k &
S3[
k,
h . k] )
by A34, A88, A89, A142;
GX . k in rng GX
by A88, A142, FUNCT_1:def 3;
then
meet (rng GX) c= GX . k
by SETFAM_1:7;
then A146:
I in GX . k
by A140;
per cases
( k = 1 or k > 1 )
by A143, XXREAL_0:1;
suppose A147:
k = 1
;
ex x being Element of bool the carrier of ((TOP-REAL n) | C) st S5[k,x]
1
in dom p
by A1, A10, A35, A39, FINSEQ_1:1;
then A148:
p . 1
= G0
by A1, A9, A30, FINSEQ_4:62, PARTFUN1:def 6;
consider g being
set such that A149:
I in g
and A150:
g in G0
by A146, A145, A147, TARSKI:def 4;
g in G
by A27, A150;
hence
ex
x being
Element of
bool the
carrier of
((TOP-REAL n) | C) st
S5[
k,
x]
by A147, A149, A150, A148;
verum suppose A151:
k > 1
;
ex x being Element of bool the carrier of ((TOP-REAL n) | C) st S5[k,x]then reconsider k1 =
k - 1 as
Nat ;
A152:
k1 + 1
= k
;
then A153:
k1 < len the
Enumeration of
A
by A144, NAT_1:13;
k1 >= 1
by A151, A152, NAT_1:13;
then A154:
S1[
k1,
p /. k1,
p /. k]
by A31, A153;
A155:
p . k = p /. k
by A35, A142, PARTFUN1:def 6;
consider g being
set such that A156:
I in g
and A157:
g in (p . k) \ (p . (k - 1))
by A146, A145, A151, TARSKI:def 4;
A158:
not
g in p . (k - 1)
by A157, XBOOLE_0:def 5;
g in p . k
by A157;
then
ex
gg being
Subset of
((TOP-REAL n) | C) st
(
g = gg &
gg in G & (
gg c= f . (k1 + 1) or
gg in p /. k1 ) )
by A154, A155;
hence
ex
x being
Element of
bool the
carrier of
((TOP-REAL n) | C) st
S5[
k,
x]
by A156, A157, A158;
verum end;
end;
consider t being
FinSequence of
bool the
carrier of
((TOP-REAL n) | C) such that A159:
(
dom t = Seg (len the Enumeration of A) & ( for
k being
Nat st
k in Seg (len the Enumeration of A) holds
S5[
k,
t . k] ) )
from FINSEQ_1:sch 5(A141);
A160:
now for i, j being Nat st i in dom t & j in dom t & i < j holds
not t . i = t . jlet i,
j be
Nat;
( i in dom t & j in dom t & i < j implies not t . i = t . j )assume that A161:
i in dom t
and A162:
j in dom t
and A163:
i < j
;
not t . i = t . jA164:
j <= len the
Enumeration of
A
by A159, A162, FINSEQ_1:1;
defpred S6[
Nat]
means (
i <= $1 & $1
< j implies
t . i in p . $1 );
A165:
S5[
i,
t . i]
by A159, A161;
A166:
1
<= i
by A159, A161, FINSEQ_1:1;
A167:
for
k being
Nat st
S6[
k] holds
S6[
k + 1]
proof
let k be
Nat;
( S6[k] implies S6[k + 1] )
assume A168:
S6[
k]
;
S6[k + 1]
set k1 =
k + 1;
assume that A169:
i <= k + 1
and A170:
k + 1
< j
;
t . i in p . (k + 1)
A171:
k < j
by A170, NAT_1:13;
per cases
( i = k + 1 or i <= k )
by A169, NAT_1:8;
suppose A172:
i <= k
;
t . i in p . (k + 1)
( 1
<= k + 1 &
k + 1
<= len the
Enumeration of
A )
by A166, A164, A169, A170, XXREAL_0:2;
then A173:
k + 1
in dom p
by A35, FINSEQ_1:1;
A174:
k < len the
Enumeration of
A
by A164, A171, XXREAL_0:2;
A175:
1
<= k
by A166, A172, XXREAL_0:2;
then
k in dom p
by A35, A174, FINSEQ_1:1;
then A176:
p . k = p /. k
by PARTFUN1:def 6;
S1[
k,
p /. k,
p /. (k + 1)]
by A31, A175, A174;
then
p . (k + 1) = { g where g is Subset of ((TOP-REAL n) | C) : ( g in G & ( g c= f . (k + 1) or g in p . k ) ) }
by A173, A176, PARTFUN1:def 6;
hence
t . i in p . (k + 1)
by A165, A168, A170, A172, NAT_1:13;
verum
end; A177:
S6[
0 ]
by A165;
A178:
for
k being
Nat holds
S6[
k]
from NAT_1:sch 2(A177, A167);
reconsider j1 =
j - 1 as
Nat by A163;
assume A179:
t . i = t . j
;
contradictionA180:
j1 + 1
= j
;
then A181:
j1 < j
by NAT_1:13;
A182:
j <> 1
by A159, A161, A163, FINSEQ_1:1;
i <= j1
by A163, A180, NAT_1:13;
then
t . i in p . j1
by A181, A178;
hence
contradiction
by A159, A162, A179, A182;
verum end;
now for x1, x2 being object st x1 in dom t & x2 in dom t & t . x1 = t . x2 holds
not x1 <> x2let x1,
x2 be
object ;
( x1 in dom t & x2 in dom t & t . x1 = t . x2 implies not x1 <> x2 )assume A183:
(
x1 in dom t &
x2 in dom t )
;
( t . x1 = t . x2 implies not x1 <> x2 )then reconsider i1 =
x1,
i2 =
x2 as
Nat ;
assume A184:
t . x1 = t . x2
;
not x1 <> x2assume
x1 <> x2
;
contradictionthen
(
i1 > i2 or
i1 < i2 )
by XXREAL_0:1;
hence
contradiction
by A160, A183, A184;
verum end;
then
t is
one-to-one
by FUNCT_1:def 4;
then A185:
card (rng t) =
len t
by FINSEQ_4:62
.=
len the
Enumeration of
A
by A159, FINSEQ_1:def 3
.=
n + 1
by A1, A9, FINSEQ_4:62
;
then A186:
not
rng t is
empty
;
A189:
rng t c= G
n < card (rng t)
by A185, NAT_1:13;
then
card (Segm n) in card (Segm (card (rng t)))
by NAT_1:41;
then
n1 + 1
in card (rng t)
;
then
meet (rng t) is
empty
by A26, A189, TOPDIM_2:2;
hence
contradiction
by A186, A187, SETFAM_1:def 1;
verum
end;
( ind (conv A) <= ind (TOP-REAL n) & ind (TOP-REAL n) <= n )
by TOPDIM_1:20, TOPDIM_2:21;
then
ind (conv A) <= n
by XXREAL_0:2;
hence
ind (conv A) = n
by A2, XXREAL_0:1; verum