let n, k be Nat; :: thesis: for A being non empty finite affinely-independent Subset of (TOP-REAL n) st k < card A holds

for E being Enumeration of A st E . (len E) = 0* n holds

for P being Subset of (TOP-REAL k)

for B being Subset of ((TOP-REAL n) | (Affin A)) st B = { v where v is Element of ((TOP-REAL n) | (Affin A)) : (v |-- E) | k in P } holds

( P is open iff B is open )

set TRn = TOP-REAL n;

let A be non empty finite affinely-independent Subset of (TOP-REAL n); :: thesis: ( k < card A implies for E being Enumeration of A st E . (len E) = 0* n holds

for P being Subset of (TOP-REAL k)

for B being Subset of ((TOP-REAL n) | (Affin A)) st B = { v where v is Element of ((TOP-REAL n) | (Affin A)) : (v |-- E) | k in P } holds

( P is open iff B is open ) )

assume A1: k < card A ; :: thesis: for E being Enumeration of A st E . (len E) = 0* n holds

for P being Subset of (TOP-REAL k)

for B being Subset of ((TOP-REAL n) | (Affin A)) st B = { v where v is Element of ((TOP-REAL n) | (Affin A)) : (v |-- E) | k in P } holds

( P is open iff B is open )

reconsider c1 = (card A) - 1 as Element of NAT by NAT_1:14, NAT_1:21;

set AA = Affin A;

let E be Enumeration of A; :: thesis: ( E . (len E) = 0* n implies for P being Subset of (TOP-REAL k)

for B being Subset of ((TOP-REAL n) | (Affin A)) st B = { v where v is Element of ((TOP-REAL n) | (Affin A)) : (v |-- E) | k in P } holds

( P is open iff B is open ) )

assume A2: E . (len E) = 0* n ; :: thesis: for P being Subset of (TOP-REAL k)

for B being Subset of ((TOP-REAL n) | (Affin A)) st B = { v where v is Element of ((TOP-REAL n) | (Affin A)) : (v |-- E) | k in P } holds

( P is open iff B is open )

A3: rng E = A by Def1;

then A4: len E = card A by FINSEQ_4:62;

then A5: len E >= 1 by NAT_1:14;

then A6: len E in dom E by FINSEQ_3:25;

then A7: 0* n in rng E by A2, FUNCT_1:def 3;

A8: 0. (TOP-REAL n) = 0* n by EUCLID:66;

then A9: 0. (TOP-REAL n) in A by A2, A3, A6, FUNCT_1:def 3;

then A10: A \ {(0. (TOP-REAL n))} is linearly-independent by RLAFFIN1:46;

card A <= 1 + (dim (TOP-REAL n)) by Th5;

then c1 + 1 <= 1 + n by Th4;

then A11: c1 <= n by XREAL_1:6;

set nc = n -' c1;

let P be Subset of (TOP-REAL k); :: thesis: for B being Subset of ((TOP-REAL n) | (Affin A)) st B = { v where v is Element of ((TOP-REAL n) | (Affin A)) : (v |-- E) | k in P } holds

( P is open iff B is open )

let B be Subset of ((TOP-REAL n) | (Affin A)); :: thesis: ( B = { v where v is Element of ((TOP-REAL n) | (Affin A)) : (v |-- E) | k in P } implies ( P is open iff B is open ) )

assume A12: B = { v where v is Element of ((TOP-REAL n) | (Affin A)) : (v |-- E) | k in P } ; :: thesis: ( P is open iff B is open )

A13: [#] ((TOP-REAL n) | (Affin A)) = Affin A by PRE_TOPC:def 5;

consider F being FinSequence such that

A14: rng F = A \ {(0. (TOP-REAL n))} and

A15: F is one-to-one by FINSEQ_4:58;

set V = n -VectSp_over F_Real;

reconsider Bn = MX2FinS (1. (F_Real,n)) as OrdBasis of n -VectSp_over F_Real by MATRLIN2:45;

len Bn = n by MATRTOP1:19;

then len (FinS2MX (Bn | c1)) = c1 by A11, FINSEQ_1:59;

then reconsider BnC = FinS2MX (Bn | c1) as Matrix of c1,n,F_Real ;

reconsider MBC = Mx2Tran BnC as Function ;

A16: c1 + 1 = card A ;

A17: len F = card (A \ {(0. (TOP-REAL n))}) by A14, A15, FINSEQ_4:62

.= c1 by A9, A16, STIRL2_1:55 ;

set MBc = Mx2Tran BnC;

set TRc = TOP-REAL c1;

A18: ( dom (Mx2Tran BnC) = [#] (TOP-REAL c1) & (Mx2Tran BnC) . (0. (TOP-REAL c1)) = 0. (TOP-REAL n) ) by FUNCT_2:def 1, MATRTOP1:29;

rng Bn is Basis of (n -VectSp_over F_Real) by MATRLIN:def 2;

then rng Bn is linearly-independent by VECTSP_7:def 3;

then A19: rng (Bn | c1) is linearly-independent by RELAT_1:70, VECTSP_7:1;

reconsider F = F as FinSequence of (TOP-REAL n) by A14, FINSEQ_1:def 4;

[#] (Lin (rng (Bn | (len F)))) c= the carrier of (n -VectSp_over F_Real) by VECTSP_4:def 2;

then reconsider BF = [#] (Lin (rng (Bn | (len F)))) as Subset of (TOP-REAL n) by Lm3;

A20: rng MBC = BF by A17, MATRTOP2:18;

consider M being Matrix of n,F_Real such that

A21: M is invertible and

A22: M | (len F) = F by A10, A14, A15, MATRTOP2:19;

set MTI = Mx2Tran (M ~);

A23: [#] ((TOP-REAL n) | BF) = BF by PRE_TOPC:def 5;

M ~ is invertible by A21, MATRIX_6:16;

then A24: Det (M ~) <> 0. F_Real by LAPLACE:34;

then A25: the_rank_of (M ~) = n by MATRIX13:83;

then reconsider MTe = (Mx2Tran (M ~)) * E as Enumeration of (Mx2Tran (M ~)) .: A by Th15;

A26: rng MTe = (Mx2Tran (M ~)) .: A by Def1;

( dom (Mx2Tran (M ~)) = [#] (TOP-REAL n) & Mx2Tran (M ~) is one-to-one ) by A24, FUNCT_2:def 1, MATRTOP1:40;

then A,(Mx2Tran (M ~)) .: A are_equipotent by CARD_1:33;

then A27: card A = card ((Mx2Tran (M ~)) .: A) by CARD_1:5;

then len MTe = len E by A4, A26, FINSEQ_4:62;

then len E in dom MTe by A5, FINSEQ_3:25;

then A28: MTe . (len E) = (Mx2Tran (M ~)) . (0. (TOP-REAL n)) by A2, A8, FUNCT_1:12

.= 0. (TOP-REAL n) by MATRTOP1:29 ;

set MT = Mx2Tran M;

Affin A = [#] (Lin A) by A3, A7, Th11

.= [#] (Lin (rng F)) by A14, Lm2 ;

then A29: (Mx2Tran M) .: BF = Affin A by A10, A14, A15, A21, A22, MATRTOP2:21;

then A30: rng ((Mx2Tran M) | BF) = Affin A by RELAT_1:115;

A31: dom (Mx2Tran M) = [#] (TOP-REAL n) by FUNCT_2:def 1;

then dom ((Mx2Tran M) | BF) = BF by RELAT_1:62;

then reconsider MT1 = (Mx2Tran M) | BF as Function of ((TOP-REAL n) | BF),((TOP-REAL n) | (Affin A)) by A13, A23, A30, FUNCT_2:1;

reconsider MT = Mx2Tran M as Function ;

A32: Det M <> 0. F_Real by A21, LAPLACE:34;

then A33: MT " = Mx2Tran (M ~) by MATRTOP1:43;

MT1 is being_homeomorphism by A21, A29, METRIZTS:2;

then A34: ( MT1 " B is open iff B is open ) by TOPGRP_1:26;

set nc0 = (n -' c1) |-> 0;

set Vc1 = { (v ^ ((n -' c1) |-> 0)) where v is Element of (TOP-REAL c1) : verum } ;

A35: n -' c1 = n - c1 by A11, XREAL_1:233;

then A36: n = c1 + (n -' c1) ;

A37: MT is one-to-one by A32, MATRTOP1:40;

then A38: MT " (Affin A) = BF by A29, A31, FUNCT_1:94;

A39: MT " A c= MT " (Affin A) by RELAT_1:143, RLAFFIN1:49;

then A40: (Mx2Tran (M ~)) .: A c= BF by A33, A37, A38, FUNCT_1:85;

Bn is one-to-one by MATRLIN:def 2;

then Bn | c1 is one-to-one by FUNCT_1:52;

then A41: the_rank_of BnC = c1 by A19, MATRIX13:121;

then A42: MBC is one-to-one by MATRTOP1:39;

then A43: dom (MBC ") = rng MBC by FUNCT_1:33;

then reconsider MBCe = (MBC ") * MTe as FinSequence by A20, A26, A40, FINSEQ_1:16;

A44: rng MBCe = (MBC ") .: ((Mx2Tran (M ~)) .: A) by A26, RELAT_1:127;

(Mx2Tran (M ~)) .: A is affinely-independent by A25, MATRTOP2:24;

then (Mx2Tran BnC) " ((Mx2Tran (M ~)) .: A) is affinely-independent by A41, MATRTOP2:27;

then reconsider R = rng MBCe as finite affinely-independent Subset of (TOP-REAL c1) by A42, A44, FUNCT_1:85;

reconsider MBCe = MBCe as Enumeration of R by A42, Def1;

reconsider MBCeE = (Mx2Tran BnC) * MBCe as Enumeration of (Mx2Tran BnC) .: R by A41, Th15;

MBC * (MBC ") = id (rng MBC) by A42, FUNCT_1:39;

then A45: MBCeE = (id (rng MBC)) * MTe by RELAT_1:36

.= MTe by A20, A26, A40, RELAT_1:53 ;

set PPP = { v where v is Element of (TOP-REAL c1) : (v |-- MBCe) | k in P } ;

A46: { v where v is Element of (TOP-REAL c1) : (v |-- MBCe) | k in P } c= [#] (TOP-REAL c1)

A48: MT " B c= MT " (Affin A) by A13, RELAT_1:143;

A49: (Mx2Tran (M ~)) .: A,R are_equipotent by A20, A42, A43, A40, A44, CARD_1:33;

then A50: c1 + 1 = card R by A27, CARD_1:5;

then A51: ( k <= c1 & not R is empty ) by A1, NAT_1:13;

reconsider PPP = { v where v is Element of (TOP-REAL c1) : (v |-- MBCe) | k in P } as Subset of (TOP-REAL c1) by A46;

set nPP = { v where v is Element of (TOP-REAL n) : ( v | c1 in PPP & v in BF ) } ;

dim (TOP-REAL c1) = c1 by Th4;

then A52: Affin R = [#] (TOP-REAL c1) by A50, Th6;

A53: (Mx2Tran BnC) .: R = MBC .: ((MBC ") .: ((Mx2Tran (M ~)) .: A)) by A26, RELAT_1:127

.= (MBC * (MBC ")) .: ((Mx2Tran (M ~)) .: A) by RELAT_1:126

.= (id (rng MBC)) .: ((Mx2Tran (M ~)) .: A) by A42, FUNCT_1:39

.= (Mx2Tran (M ~)) .: A by A47, A38, A39, A20, FUNCT_1:92 ;

A54: MT " B c= { v where v is Element of (TOP-REAL n) : ( v | c1 in PPP & v in BF ) }

A68: { v where v is Element of (TOP-REAL n) : ( v | c1 in PPP & v in BF ) } c= MT " B

then len E in dom MBCe by A5, FINSEQ_3:25;

then MBCe . (len E) = (MBC ") . (0. (TOP-REAL n)) by A28, FUNCT_1:12

.= 0. (TOP-REAL c1) by A42, A18, FUNCT_1:34 ;

then A81: MBCe . (len MBCe) = 0* c1 by A80, EUCLID:70;

MT1 " B = BF /\ (MT " B) by FUNCT_1:70

.= MT " B by A13, A38, RELAT_1:143, XBOOLE_1:28 ;

then MT1 " B = { v where v is Element of (TOP-REAL n) : ( v | c1 in PPP & v in BF ) } by A54, A68;

then A82: ( PPP is open iff B is open ) by A34, A67, A36, Th8;

card R = c1 + 1 by A27, A49, CARD_1:5;

hence ( P is open iff B is open ) by A81, A82, A51, Lm7; :: thesis: verum

for E being Enumeration of A st E . (len E) = 0* n holds

for P being Subset of (TOP-REAL k)

for B being Subset of ((TOP-REAL n) | (Affin A)) st B = { v where v is Element of ((TOP-REAL n) | (Affin A)) : (v |-- E) | k in P } holds

( P is open iff B is open )

set TRn = TOP-REAL n;

let A be non empty finite affinely-independent Subset of (TOP-REAL n); :: thesis: ( k < card A implies for E being Enumeration of A st E . (len E) = 0* n holds

for P being Subset of (TOP-REAL k)

for B being Subset of ((TOP-REAL n) | (Affin A)) st B = { v where v is Element of ((TOP-REAL n) | (Affin A)) : (v |-- E) | k in P } holds

( P is open iff B is open ) )

assume A1: k < card A ; :: thesis: for E being Enumeration of A st E . (len E) = 0* n holds

for P being Subset of (TOP-REAL k)

for B being Subset of ((TOP-REAL n) | (Affin A)) st B = { v where v is Element of ((TOP-REAL n) | (Affin A)) : (v |-- E) | k in P } holds

( P is open iff B is open )

reconsider c1 = (card A) - 1 as Element of NAT by NAT_1:14, NAT_1:21;

set AA = Affin A;

let E be Enumeration of A; :: thesis: ( E . (len E) = 0* n implies for P being Subset of (TOP-REAL k)

for B being Subset of ((TOP-REAL n) | (Affin A)) st B = { v where v is Element of ((TOP-REAL n) | (Affin A)) : (v |-- E) | k in P } holds

( P is open iff B is open ) )

assume A2: E . (len E) = 0* n ; :: thesis: for P being Subset of (TOP-REAL k)

for B being Subset of ((TOP-REAL n) | (Affin A)) st B = { v where v is Element of ((TOP-REAL n) | (Affin A)) : (v |-- E) | k in P } holds

( P is open iff B is open )

A3: rng E = A by Def1;

then A4: len E = card A by FINSEQ_4:62;

then A5: len E >= 1 by NAT_1:14;

then A6: len E in dom E by FINSEQ_3:25;

then A7: 0* n in rng E by A2, FUNCT_1:def 3;

A8: 0. (TOP-REAL n) = 0* n by EUCLID:66;

then A9: 0. (TOP-REAL n) in A by A2, A3, A6, FUNCT_1:def 3;

then A10: A \ {(0. (TOP-REAL n))} is linearly-independent by RLAFFIN1:46;

card A <= 1 + (dim (TOP-REAL n)) by Th5;

then c1 + 1 <= 1 + n by Th4;

then A11: c1 <= n by XREAL_1:6;

set nc = n -' c1;

let P be Subset of (TOP-REAL k); :: thesis: for B being Subset of ((TOP-REAL n) | (Affin A)) st B = { v where v is Element of ((TOP-REAL n) | (Affin A)) : (v |-- E) | k in P } holds

( P is open iff B is open )

let B be Subset of ((TOP-REAL n) | (Affin A)); :: thesis: ( B = { v where v is Element of ((TOP-REAL n) | (Affin A)) : (v |-- E) | k in P } implies ( P is open iff B is open ) )

assume A12: B = { v where v is Element of ((TOP-REAL n) | (Affin A)) : (v |-- E) | k in P } ; :: thesis: ( P is open iff B is open )

A13: [#] ((TOP-REAL n) | (Affin A)) = Affin A by PRE_TOPC:def 5;

consider F being FinSequence such that

A14: rng F = A \ {(0. (TOP-REAL n))} and

A15: F is one-to-one by FINSEQ_4:58;

set V = n -VectSp_over F_Real;

reconsider Bn = MX2FinS (1. (F_Real,n)) as OrdBasis of n -VectSp_over F_Real by MATRLIN2:45;

len Bn = n by MATRTOP1:19;

then len (FinS2MX (Bn | c1)) = c1 by A11, FINSEQ_1:59;

then reconsider BnC = FinS2MX (Bn | c1) as Matrix of c1,n,F_Real ;

reconsider MBC = Mx2Tran BnC as Function ;

A16: c1 + 1 = card A ;

A17: len F = card (A \ {(0. (TOP-REAL n))}) by A14, A15, FINSEQ_4:62

.= c1 by A9, A16, STIRL2_1:55 ;

set MBc = Mx2Tran BnC;

set TRc = TOP-REAL c1;

A18: ( dom (Mx2Tran BnC) = [#] (TOP-REAL c1) & (Mx2Tran BnC) . (0. (TOP-REAL c1)) = 0. (TOP-REAL n) ) by FUNCT_2:def 1, MATRTOP1:29;

rng Bn is Basis of (n -VectSp_over F_Real) by MATRLIN:def 2;

then rng Bn is linearly-independent by VECTSP_7:def 3;

then A19: rng (Bn | c1) is linearly-independent by RELAT_1:70, VECTSP_7:1;

reconsider F = F as FinSequence of (TOP-REAL n) by A14, FINSEQ_1:def 4;

[#] (Lin (rng (Bn | (len F)))) c= the carrier of (n -VectSp_over F_Real) by VECTSP_4:def 2;

then reconsider BF = [#] (Lin (rng (Bn | (len F)))) as Subset of (TOP-REAL n) by Lm3;

A20: rng MBC = BF by A17, MATRTOP2:18;

consider M being Matrix of n,F_Real such that

A21: M is invertible and

A22: M | (len F) = F by A10, A14, A15, MATRTOP2:19;

set MTI = Mx2Tran (M ~);

A23: [#] ((TOP-REAL n) | BF) = BF by PRE_TOPC:def 5;

M ~ is invertible by A21, MATRIX_6:16;

then A24: Det (M ~) <> 0. F_Real by LAPLACE:34;

then A25: the_rank_of (M ~) = n by MATRIX13:83;

then reconsider MTe = (Mx2Tran (M ~)) * E as Enumeration of (Mx2Tran (M ~)) .: A by Th15;

A26: rng MTe = (Mx2Tran (M ~)) .: A by Def1;

( dom (Mx2Tran (M ~)) = [#] (TOP-REAL n) & Mx2Tran (M ~) is one-to-one ) by A24, FUNCT_2:def 1, MATRTOP1:40;

then A,(Mx2Tran (M ~)) .: A are_equipotent by CARD_1:33;

then A27: card A = card ((Mx2Tran (M ~)) .: A) by CARD_1:5;

then len MTe = len E by A4, A26, FINSEQ_4:62;

then len E in dom MTe by A5, FINSEQ_3:25;

then A28: MTe . (len E) = (Mx2Tran (M ~)) . (0. (TOP-REAL n)) by A2, A8, FUNCT_1:12

.= 0. (TOP-REAL n) by MATRTOP1:29 ;

set MT = Mx2Tran M;

Affin A = [#] (Lin A) by A3, A7, Th11

.= [#] (Lin (rng F)) by A14, Lm2 ;

then A29: (Mx2Tran M) .: BF = Affin A by A10, A14, A15, A21, A22, MATRTOP2:21;

then A30: rng ((Mx2Tran M) | BF) = Affin A by RELAT_1:115;

A31: dom (Mx2Tran M) = [#] (TOP-REAL n) by FUNCT_2:def 1;

then dom ((Mx2Tran M) | BF) = BF by RELAT_1:62;

then reconsider MT1 = (Mx2Tran M) | BF as Function of ((TOP-REAL n) | BF),((TOP-REAL n) | (Affin A)) by A13, A23, A30, FUNCT_2:1;

reconsider MT = Mx2Tran M as Function ;

A32: Det M <> 0. F_Real by A21, LAPLACE:34;

then A33: MT " = Mx2Tran (M ~) by MATRTOP1:43;

MT1 is being_homeomorphism by A21, A29, METRIZTS:2;

then A34: ( MT1 " B is open iff B is open ) by TOPGRP_1:26;

set nc0 = (n -' c1) |-> 0;

set Vc1 = { (v ^ ((n -' c1) |-> 0)) where v is Element of (TOP-REAL c1) : verum } ;

A35: n -' c1 = n - c1 by A11, XREAL_1:233;

then A36: n = c1 + (n -' c1) ;

A37: MT is one-to-one by A32, MATRTOP1:40;

then A38: MT " (Affin A) = BF by A29, A31, FUNCT_1:94;

A39: MT " A c= MT " (Affin A) by RELAT_1:143, RLAFFIN1:49;

then A40: (Mx2Tran (M ~)) .: A c= BF by A33, A37, A38, FUNCT_1:85;

Bn is one-to-one by MATRLIN:def 2;

then Bn | c1 is one-to-one by FUNCT_1:52;

then A41: the_rank_of BnC = c1 by A19, MATRIX13:121;

then A42: MBC is one-to-one by MATRTOP1:39;

then A43: dom (MBC ") = rng MBC by FUNCT_1:33;

then reconsider MBCe = (MBC ") * MTe as FinSequence by A20, A26, A40, FINSEQ_1:16;

A44: rng MBCe = (MBC ") .: ((Mx2Tran (M ~)) .: A) by A26, RELAT_1:127;

(Mx2Tran (M ~)) .: A is affinely-independent by A25, MATRTOP2:24;

then (Mx2Tran BnC) " ((Mx2Tran (M ~)) .: A) is affinely-independent by A41, MATRTOP2:27;

then reconsider R = rng MBCe as finite affinely-independent Subset of (TOP-REAL c1) by A42, A44, FUNCT_1:85;

reconsider MBCe = MBCe as Enumeration of R by A42, Def1;

reconsider MBCeE = (Mx2Tran BnC) * MBCe as Enumeration of (Mx2Tran BnC) .: R by A41, Th15;

MBC * (MBC ") = id (rng MBC) by A42, FUNCT_1:39;

then A45: MBCeE = (id (rng MBC)) * MTe by RELAT_1:36

.= MTe by A20, A26, A40, RELAT_1:53 ;

set PPP = { v where v is Element of (TOP-REAL c1) : (v |-- MBCe) | k in P } ;

A46: { v where v is Element of (TOP-REAL c1) : (v |-- MBCe) | k in P } c= [#] (TOP-REAL c1)

proof

A47:
(Mx2Tran (M ~)) .: A = MT " A
by A33, A37, FUNCT_1:85;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { v where v is Element of (TOP-REAL c1) : (v |-- MBCe) | k in P } or x in [#] (TOP-REAL c1) )

assume x in { v where v is Element of (TOP-REAL c1) : (v |-- MBCe) | k in P } ; :: thesis: x in [#] (TOP-REAL c1)

then ex v being Element of (TOP-REAL c1) st

( x = v & (v |-- MBCe) | k in P ) ;

hence x in [#] (TOP-REAL c1) ; :: thesis: verum

end;assume x in { v where v is Element of (TOP-REAL c1) : (v |-- MBCe) | k in P } ; :: thesis: x in [#] (TOP-REAL c1)

then ex v being Element of (TOP-REAL c1) st

( x = v & (v |-- MBCe) | k in P ) ;

hence x in [#] (TOP-REAL c1) ; :: thesis: verum

A48: MT " B c= MT " (Affin A) by A13, RELAT_1:143;

A49: (Mx2Tran (M ~)) .: A,R are_equipotent by A20, A42, A43, A40, A44, CARD_1:33;

then A50: c1 + 1 = card R by A27, CARD_1:5;

then A51: ( k <= c1 & not R is empty ) by A1, NAT_1:13;

reconsider PPP = { v where v is Element of (TOP-REAL c1) : (v |-- MBCe) | k in P } as Subset of (TOP-REAL c1) by A46;

set nPP = { v where v is Element of (TOP-REAL n) : ( v | c1 in PPP & v in BF ) } ;

dim (TOP-REAL c1) = c1 by Th4;

then A52: Affin R = [#] (TOP-REAL c1) by A50, Th6;

A53: (Mx2Tran BnC) .: R = MBC .: ((MBC ") .: ((Mx2Tran (M ~)) .: A)) by A26, RELAT_1:127

.= (MBC * (MBC ")) .: ((Mx2Tran (M ~)) .: A) by RELAT_1:126

.= (id (rng MBC)) .: ((Mx2Tran (M ~)) .: A) by A42, FUNCT_1:39

.= (Mx2Tran (M ~)) .: A by A47, A38, A39, A20, FUNCT_1:92 ;

A54: MT " B c= { v where v is Element of (TOP-REAL n) : ( v | c1 in PPP & v in BF ) }

proof

A63:
BF c= { (v ^ ((n -' c1) |-> 0)) where v is Element of (TOP-REAL c1) : verum }
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in MT " B or x in { v where v is Element of (TOP-REAL n) : ( v | c1 in PPP & v in BF ) } )

assume A55: x in MT " B ; :: thesis: x in { v where v is Element of (TOP-REAL n) : ( v | c1 in PPP & v in BF ) }

then reconsider w = x as Element of ((TOP-REAL n) | BF) by A29, A23, A31, A37, A48, FUNCT_1:94;

MT . x in B by A55, FUNCT_1:def 7;

then consider v being Element of ((TOP-REAL n) | (Affin A)) such that

A56: MT . x = v and

A57: (v |-- E) | k in P by A12;

x in dom MT by A55, FUNCT_1:def 7;

then A58: (Mx2Tran (M ~)) . v = x by A33, A37, A56, FUNCT_1:34;

x in BF by A38, A48, A55;

then reconsider W = x as Element of (TOP-REAL n) ;

A59: v in Affin A by A13;

consider u being object such that

A60: u in dom (Mx2Tran BnC) and

A61: (Mx2Tran BnC) . u = w by A38, A48, A20, A55, FUNCT_1:def 3;

A62: W | c1 = u by A60, A61, MATRTOP1:38;

reconsider u = u as Element of (TOP-REAL c1) by A60;

u |-- MBCe = w |-- MTe by A61, A53, A45, A41, A52, Th19

.= v |-- E by A25, A58, A59, Th19 ;

then u in PPP by A57;

hence x in { v where v is Element of (TOP-REAL n) : ( v | c1 in PPP & v in BF ) } by A38, A48, A55, A62; :: thesis: verum

end;assume A55: x in MT " B ; :: thesis: x in { v where v is Element of (TOP-REAL n) : ( v | c1 in PPP & v in BF ) }

then reconsider w = x as Element of ((TOP-REAL n) | BF) by A29, A23, A31, A37, A48, FUNCT_1:94;

MT . x in B by A55, FUNCT_1:def 7;

then consider v being Element of ((TOP-REAL n) | (Affin A)) such that

A56: MT . x = v and

A57: (v |-- E) | k in P by A12;

x in dom MT by A55, FUNCT_1:def 7;

then A58: (Mx2Tran (M ~)) . v = x by A33, A37, A56, FUNCT_1:34;

x in BF by A38, A48, A55;

then reconsider W = x as Element of (TOP-REAL n) ;

A59: v in Affin A by A13;

consider u being object such that

A60: u in dom (Mx2Tran BnC) and

A61: (Mx2Tran BnC) . u = w by A38, A48, A20, A55, FUNCT_1:def 3;

A62: W | c1 = u by A60, A61, MATRTOP1:38;

reconsider u = u as Element of (TOP-REAL c1) by A60;

u |-- MBCe = w |-- MTe by A61, A53, A45, A41, A52, Th19

.= v |-- E by A25, A58, A59, Th19 ;

then u in PPP by A57;

hence x in { v where v is Element of (TOP-REAL n) : ( v | c1 in PPP & v in BF ) } by A38, A48, A55, A62; :: thesis: verum

proof

{ (v ^ ((n -' c1) |-> 0)) where v is Element of (TOP-REAL c1) : verum } c= BF
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in BF or x in { (v ^ ((n -' c1) |-> 0)) where v is Element of (TOP-REAL c1) : verum } )

assume A64: x in BF ; :: thesis: x in { (v ^ ((n -' c1) |-> 0)) where v is Element of (TOP-REAL c1) : verum }

then reconsider f = x as Element of (TOP-REAL n) ;

len f = n by CARD_1:def 7;

then len (f | c1) = c1 by A11, FINSEQ_1:59;

then f | c1 is c1 -element by CARD_1:def 7;

then A65: f | c1 is Element of (TOP-REAL c1) by Lm1;

f in Lin (rng (Bn | c1)) by A17, A64;

then f = (f | c1) ^ ((n -' c1) |-> 0) by MATRTOP2:20;

hence x in { (v ^ ((n -' c1) |-> 0)) where v is Element of (TOP-REAL c1) : verum } by A65; :: thesis: verum

end;assume A64: x in BF ; :: thesis: x in { (v ^ ((n -' c1) |-> 0)) where v is Element of (TOP-REAL c1) : verum }

then reconsider f = x as Element of (TOP-REAL n) ;

len f = n by CARD_1:def 7;

then len (f | c1) = c1 by A11, FINSEQ_1:59;

then f | c1 is c1 -element by CARD_1:def 7;

then A65: f | c1 is Element of (TOP-REAL c1) by Lm1;

f in Lin (rng (Bn | c1)) by A17, A64;

then f = (f | c1) ^ ((n -' c1) |-> 0) by MATRTOP2:20;

hence x in { (v ^ ((n -' c1) |-> 0)) where v is Element of (TOP-REAL c1) : verum } by A65; :: thesis: verum

proof

then A67:
BF = { (v ^ ((n -' c1) |-> 0)) where v is Element of (TOP-REAL c1) : verum }
by A63;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (v ^ ((n -' c1) |-> 0)) where v is Element of (TOP-REAL c1) : verum } or x in BF )

assume x in { (v ^ ((n -' c1) |-> 0)) where v is Element of (TOP-REAL c1) : verum } ; :: thesis: x in BF

then consider v being Element of (TOP-REAL c1) such that

A66: x = v ^ ((n -' c1) |-> 0) and

verum ;

len v = c1 by CARD_1:def 7;

then (v ^ ((n -' c1) |-> 0)) | c1 = (v ^ ((n -' c1) |-> 0)) | (dom v) by FINSEQ_1:def 3

.= v by FINSEQ_1:21 ;

then v ^ ((n -' c1) |-> 0) in Lin (rng (Bn | c1)) by A35, MATRTOP2:20;

hence x in BF by A17, A66; :: thesis: verum

end;assume x in { (v ^ ((n -' c1) |-> 0)) where v is Element of (TOP-REAL c1) : verum } ; :: thesis: x in BF

then consider v being Element of (TOP-REAL c1) such that

A66: x = v ^ ((n -' c1) |-> 0) and

verum ;

len v = c1 by CARD_1:def 7;

then (v ^ ((n -' c1) |-> 0)) | c1 = (v ^ ((n -' c1) |-> 0)) | (dom v) by FINSEQ_1:def 3

.= v by FINSEQ_1:21 ;

then v ^ ((n -' c1) |-> 0) in Lin (rng (Bn | c1)) by A35, MATRTOP2:20;

hence x in BF by A17, A66; :: thesis: verum

A68: { v where v is Element of (TOP-REAL n) : ( v | c1 in PPP & v in BF ) } c= MT " B

proof

A80:
len MBCe = len E
by A4, A50, FINSEQ_4:62;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { v where v is Element of (TOP-REAL n) : ( v | c1 in PPP & v in BF ) } or x in MT " B )

assume x in { v where v is Element of (TOP-REAL n) : ( v | c1 in PPP & v in BF ) } ; :: thesis: x in MT " B

then consider v being Element of (TOP-REAL n) such that

A69: x = v and

A70: v | c1 in PPP and

A71: v in BF ;

consider v1 being Element of (TOP-REAL c1) such that

A72: v = v1 ^ ((n -' c1) |-> 0) by A67, A71;

consider u being Element of (TOP-REAL c1) such that

A73: u = v | c1 and

A74: (u |-- MBCe) | k in P by A70;

set w = (Mx2Tran BnC) . u;

A75: (Mx2Tran BnC) . u = (Mx2Tran (M ~)) . (MT . ((Mx2Tran BnC) . u)) by A31, A33, A37, FUNCT_1:34;

dom (Mx2Tran BnC) = [#] (TOP-REAL c1) by FUNCT_2:def 1;

then A76: (Mx2Tran BnC) . u in BF by A20, FUNCT_1:def 3;

then A77: MT . ((Mx2Tran BnC) . u) in Affin A by A29, A31, FUNCT_1:def 6;

u |-- MBCe = ((Mx2Tran BnC) . u) |-- MBCeE by A41, A52, Th19

.= (MT . ((Mx2Tran BnC) . u)) |-- E by A25, A75, A77, Th19, A53, A45 ;

then A78: MT . ((Mx2Tran BnC) . u) in B by A12, A13, A74, A77;

consider w1 being Element of (TOP-REAL c1) such that

A79: (Mx2Tran BnC) . u = w1 ^ ((n -' c1) |-> 0) by A67, A76;

w1 = ((Mx2Tran BnC) . u) | (dom w1) by A79, FINSEQ_1:21

.= ((Mx2Tran BnC) . u) | (Seg (len w1)) by FINSEQ_1:def 3

.= ((Mx2Tran BnC) . u) | c1 by CARD_1:def 7

.= v | c1 by A73, MATRTOP1:38

.= v | (Seg (len v1)) by CARD_1:def 7

.= v | (dom v1) by FINSEQ_1:def 3

.= v1 by A72, FINSEQ_1:21 ;

hence x in MT " B by A31, A69, A79, A72, A78, FUNCT_1:def 7; :: thesis: verum

end;assume x in { v where v is Element of (TOP-REAL n) : ( v | c1 in PPP & v in BF ) } ; :: thesis: x in MT " B

then consider v being Element of (TOP-REAL n) such that

A69: x = v and

A70: v | c1 in PPP and

A71: v in BF ;

consider v1 being Element of (TOP-REAL c1) such that

A72: v = v1 ^ ((n -' c1) |-> 0) by A67, A71;

consider u being Element of (TOP-REAL c1) such that

A73: u = v | c1 and

A74: (u |-- MBCe) | k in P by A70;

set w = (Mx2Tran BnC) . u;

A75: (Mx2Tran BnC) . u = (Mx2Tran (M ~)) . (MT . ((Mx2Tran BnC) . u)) by A31, A33, A37, FUNCT_1:34;

dom (Mx2Tran BnC) = [#] (TOP-REAL c1) by FUNCT_2:def 1;

then A76: (Mx2Tran BnC) . u in BF by A20, FUNCT_1:def 3;

then A77: MT . ((Mx2Tran BnC) . u) in Affin A by A29, A31, FUNCT_1:def 6;

u |-- MBCe = ((Mx2Tran BnC) . u) |-- MBCeE by A41, A52, Th19

.= (MT . ((Mx2Tran BnC) . u)) |-- E by A25, A75, A77, Th19, A53, A45 ;

then A78: MT . ((Mx2Tran BnC) . u) in B by A12, A13, A74, A77;

consider w1 being Element of (TOP-REAL c1) such that

A79: (Mx2Tran BnC) . u = w1 ^ ((n -' c1) |-> 0) by A67, A76;

w1 = ((Mx2Tran BnC) . u) | (dom w1) by A79, FINSEQ_1:21

.= ((Mx2Tran BnC) . u) | (Seg (len w1)) by FINSEQ_1:def 3

.= ((Mx2Tran BnC) . u) | c1 by CARD_1:def 7

.= v | c1 by A73, MATRTOP1:38

.= v | (Seg (len v1)) by CARD_1:def 7

.= v | (dom v1) by FINSEQ_1:def 3

.= v1 by A72, FINSEQ_1:21 ;

hence x in MT " B by A31, A69, A79, A72, A78, FUNCT_1:def 7; :: thesis: verum

then len E in dom MBCe by A5, FINSEQ_3:25;

then MBCe . (len E) = (MBC ") . (0. (TOP-REAL n)) by A28, FUNCT_1:12

.= 0. (TOP-REAL c1) by A42, A18, FUNCT_1:34 ;

then A81: MBCe . (len MBCe) = 0* c1 by A80, EUCLID:70;

MT1 " B = BF /\ (MT " B) by FUNCT_1:70

.= MT " B by A13, A38, RELAT_1:143, XBOOLE_1:28 ;

then MT1 " B = { v where v is Element of (TOP-REAL n) : ( v | c1 in PPP & v in BF ) } by A54, A68;

then A82: ( PPP is open iff B is open ) by A34, A67, A36, Th8;

card R = c1 + 1 by A27, A49, CARD_1:5;

hence ( P is open iff B is open ) by A81, A82, A51, Lm7; :: thesis: verum