let n, k be Nat; :: thesis: for A being non empty finite affinely-independent Subset of () st k < card A holds
for E being Enumeration of A st E . (len E) = 0* n holds
for P being Subset of ()
for B being Subset of (() | ()) st B = { v where v is Element of (() | ()) : (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 (); :: thesis: ( k < card A implies for E being Enumeration of A st E . (len E) = 0* n holds
for P being Subset of ()
for B being Subset of (() | ()) st B = { v where v is Element of (() | ()) : (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 ()
for B being Subset of (() | ()) st B = { v where v is Element of (() | ()) : (v |-- E) | k in P } holds
( P is open iff B is open )

reconsider c1 = (card A) - 1 as Element of NAT by ;
set AA = Affin A;
let E be Enumeration of A; :: thesis: ( E . (len E) = 0* n implies for P being Subset of ()
for B being Subset of (() | ()) st B = { v where v is Element of (() | ()) : (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 ()
for B being Subset of (() | ()) st B = { v where v is Element of (() | ()) : (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 ;
A8: 0. () = 0* n by EUCLID:66;
then A9: 0. () in A by ;
then A10: A \ {(0. ())} is linearly-independent by RLAFFIN1:46;
card A <= 1 + (dim ()) 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 (); :: thesis: for B being Subset of (() | ()) st B = { v where v is Element of (() | ()) : (v |-- E) | k in P } holds
( P is open iff B is open )

let B be Subset of (() | ()); :: thesis: ( B = { v where v is Element of (() | ()) : (v |-- E) | k in P } implies ( P is open iff B is open ) )
assume A12: B = { v where v is Element of (() | ()) : (v |-- E) | k in P } ; :: thesis: ( P is open iff B is open )
A13: [#] (() | ()) = Affin A by PRE_TOPC:def 5;
consider F being FinSequence such that
A14: rng F = A \ {(0. ())} 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 ;
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. ())}) by
.= c1 by ;
set MBc = Mx2Tran BnC;
set TRc = TOP-REAL c1;
A18: ( dom (Mx2Tran BnC) = [#] (TOP-REAL c1) & (Mx2Tran BnC) . (0. (TOP-REAL c1)) = 0. () ) by ;
rng Bn is Basis of () by MATRLIN:def 2;
then rng Bn is linearly-independent by VECTSP_7:def 3;
then A19: rng (Bn | c1) is linearly-independent by ;
reconsider F = F as FinSequence of () by ;
[#] (Lin (rng (Bn | (len F)))) c= the carrier of () by VECTSP_4:def 2;
then reconsider BF = [#] (Lin (rng (Bn | (len F)))) as Subset of () by Lm3;
A20: rng MBC = BF by ;
consider M being Matrix of n,F_Real such that
A21: M is invertible and
A22: M | (len F) = F by ;
set MTI = Mx2Tran (M ~);
A23: [#] (() | BF) = BF by PRE_TOPC:def 5;
M ~ is invertible by ;
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 ~)) = [#] () & Mx2Tran (M ~) is one-to-one ) by ;
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 ;
then len E in dom MTe by ;
then A28: MTe . (len E) = (Mx2Tran (M ~)) . (0. ()) by
.= 0. () by MATRTOP1:29 ;
set MT = Mx2Tran M;
Affin A = [#] (Lin A) by A3, A7, Th11
.= [#] (Lin (rng F)) by ;
then A29: (Mx2Tran M) .: BF = Affin A by ;
then A30: rng (() | BF) = Affin A by RELAT_1:115;
A31: dom () = [#] () by FUNCT_2:def 1;
then dom (() | BF) = BF by RELAT_1:62;
then reconsider MT1 = () | BF as Function of (() | BF),(() | ()) by ;
reconsider MT = Mx2Tran M as Function ;
A32: Det M <> 0. F_Real by ;
then A33: MT " = Mx2Tran (M ~) by MATRTOP1:43;
MT1 is being_homeomorphism by ;
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 ;
then A36: n = c1 + (n -' c1) ;
A37: MT is one-to-one by ;
then A38: MT " () = BF by ;
A39: MT " A c= MT " () by ;
then A40: (Mx2Tran (M ~)) .: A c= BF by ;
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 ;
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 ;
A44: rng MBCe = (MBC ") .: ((Mx2Tran (M ~)) .: A) by ;
(Mx2Tran (M ~)) .: A is affinely-independent by ;
then (Mx2Tran BnC) " ((Mx2Tran (M ~)) .: A) is affinely-independent by ;
then reconsider R = rng MBCe as finite affinely-independent Subset of (TOP-REAL c1) by ;
reconsider MBCe = MBCe as Enumeration of R by ;
reconsider MBCeE = (Mx2Tran BnC) * MBCe as Enumeration of (Mx2Tran BnC) .: R by ;
MBC * (MBC ") = id (rng MBC) by ;
then A45: MBCeE = (id (rng MBC)) * MTe by RELAT_1:36
.= MTe by ;
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
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;
A47: (Mx2Tran (M ~)) .: A = MT " A by ;
A48: MT " B c= MT " () by ;
A49: (Mx2Tran (M ~)) .: A,R are_equipotent by ;
then A50: c1 + 1 = card R by ;
then A51: ( k <= c1 & not R is empty ) by ;
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 () : ( v | c1 in PPP & v in BF ) } ;
dim (TOP-REAL c1) = c1 by Th4;
then A52: Affin R = [#] (TOP-REAL c1) by ;
A53: (Mx2Tran BnC) .: R = MBC .: ((MBC ") .: ((Mx2Tran (M ~)) .: A)) by
.= (MBC * (MBC ")) .: ((Mx2Tran (M ~)) .: A) by RELAT_1:126
.= (id (rng MBC)) .: ((Mx2Tran (M ~)) .: A) by
.= (Mx2Tran (M ~)) .: A by ;
A54: MT " B c= { v where v is Element of () : ( v | c1 in PPP & v in BF ) }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in MT " B or x in { v where v is Element of () : ( v | c1 in PPP & v in BF ) } )
assume A55: x in MT " B ; :: thesis: x in { v where v is Element of () : ( v | c1 in PPP & v in BF ) }
then reconsider w = x as Element of (() | BF) by ;
MT . x in B by ;
then consider v being Element of (() | ()) such that
A56: MT . x = v and
A57: (v |-- E) | k in P by A12;
x in dom MT by ;
then A58: (Mx2Tran (M ~)) . v = x by ;
x in BF by ;
then reconsider W = x as Element of () ;
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 ;
A62: W | c1 = u by ;
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 ;
then u in PPP by A57;
hence x in { v where v is Element of () : ( v | c1 in PPP & v in BF ) } by A38, A48, A55, A62; :: thesis: verum
end;
A63: BF c= { (v ^ ((n -' c1) |-> 0)) where v is Element of (TOP-REAL c1) : verum }
proof
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 () ;
len f = n by CARD_1:def 7;
then len (f | c1) = c1 by ;
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 ;
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;
{ (v ^ ((n -' c1) |-> 0)) where v is Element of (TOP-REAL c1) : verum } c= BF
proof
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 ;
hence x in BF by ; :: thesis: verum
end;
then A67: BF = { (v ^ ((n -' c1) |-> 0)) where v is Element of (TOP-REAL c1) : verum } by A63;
A68: { v where v is Element of () : ( v | c1 in PPP & v in BF ) } c= MT " B
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { v where v is Element of () : ( v | c1 in PPP & v in BF ) } or x in MT " B )
assume x in { v where v is Element of () : ( v | c1 in PPP & v in BF ) } ; :: thesis: x in MT " B
then consider v being Element of () 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 ;
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 ;
dom (Mx2Tran BnC) = [#] (TOP-REAL c1) by FUNCT_2:def 1;
then A76: (Mx2Tran BnC) . u in BF by ;
then A77: MT . ((Mx2Tran BnC) . u) in Affin A by ;
u |-- MBCe = ((Mx2Tran BnC) . u) |-- MBCeE by
.= (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 ;
w1 = ((Mx2Tran BnC) . u) | (dom w1) by
.= ((Mx2Tran BnC) . u) | (Seg (len w1)) by FINSEQ_1:def 3
.= ((Mx2Tran BnC) . u) | c1 by CARD_1:def 7
.= v | c1 by
.= v | (Seg (len v1)) by CARD_1:def 7
.= v | (dom v1) by FINSEQ_1:def 3
.= v1 by ;
hence x in MT " B by ; :: thesis: verum
end;
A80: len MBCe = len E by ;
then len E in dom MBCe by ;
then MBCe . (len E) = (MBC ") . (0. ()) by
.= 0. (TOP-REAL c1) by ;
then A81: MBCe . (len MBCe) = 0* c1 by ;
MT1 " B = BF /\ (MT " B) by FUNCT_1:70
.= MT " B by ;
then MT1 " B = { v where v is Element of () : ( v | c1 in PPP & v in BF ) } by ;
then A82: ( PPP is open iff B is open ) by A34, A67, A36, Th8;
card R = c1 + 1 by ;
hence ( P is open iff B is open ) by A81, A82, A51, Lm7; :: thesis: verum