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

assume A1: k <= n ; :: thesis: for A being non empty finite affinely-independent Subset of () st card A = n + 1 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 = { pn where pn is Point of () : (pn |-- E) | k in P } holds
( P is open iff B is open )

set V = n -VectSp_over F_Real;
set TRn = TOP-REAL n;
let A be non empty finite affinely-independent Subset of (); :: thesis: ( card A = n + 1 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 = { pn where pn is Point of () : (pn |-- E) | k in P } holds
( P is open iff B is open ) )

reconsider A1 = A as Subset of () by Lm3;
set TRk = TOP-REAL k;
set cA = (card A) -' 1;
assume A2: card A = n + 1 ; :: 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 = { pn where pn is Point of () : (pn |-- E) | k in P } holds
( P is open iff B is open )

dim () = n by Th4;
then A3: Affin A = [#] () by ;
0* n = 0. () by EUCLID:66;
then A4: Lin (A \ {(0* n)}) = Lin A by Lm2;
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 = { pn where pn is Point of () : (pn |-- E) | k in P } holds
( P is open iff B is open ) )

reconsider e = E as FinSequence of () by Lm3;
A5: rng E = A by Def1;
then A6: len E = card A by FINSEQ_4:62;
n < n + 1 by NAT_1:13;
then len (FinS2MX (e | n)) = n by ;
then reconsider M = FinS2MX (e | n) as Matrix of n,F_Real ;
A7: (card A) - 1 = (card A) -' 1 by ;
set MT = Mx2Tran M;
assume A8: E . (len E) = 0* n ; :: thesis: for P being Subset of ()
for B being Subset of () st B = { pn where pn is Point of () : (pn |-- E) | k in P } holds
( P is open iff B is open )

let P be Subset of (); :: thesis: for B being Subset of () st B = { pn where pn is Point of () : (pn |-- E) | k in P } holds
( P is open iff B is open )

let B be Subset of (); :: thesis: ( B = { pn where pn is Point of () : (pn |-- E) | k in P } implies ( P is open iff B is open ) )
set PP = { v where v is Element of () : v | k in P } ;
{ v where v is Element of () : v | k in P } c= the carrier of ()
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { v where v is Element of () : v | k in P } or x in the carrier of () )
assume x in { v where v is Element of () : v | k in P } ; :: thesis: x in the carrier of ()
then ex v being Element of () st
( x = v & v | k in P ) ;
hence x in the carrier of () ; :: thesis: verum
end;
then reconsider PP = { v where v is Element of () : v | k in P } as Subset of () ;
assume A9: B = { v where v is Element of () : (v |-- E) | k in P } ; :: thesis: ( P is open iff B is open )
card A >= 1 by NAT_1:14;
then len E in dom E by ;
then A10: 0* n in A by ;
then A11: ( [#] (Lin (A \ {(0* n)})) = [#] (Lin (A1 \ {(0* n)})) & rng (E | ((card A) -' 1)) = A \ {(0* n)} ) by ;
[#] (Lin A) = [#] (Lin A1) by MATRTOP2:6;
then A12: Lin () = Lin A1 by ;
then reconsider BE = E | ((card A) -' 1) as OrdBasis of Lin () by ;
rng BE is Basis of (Lin ()) by MATRLIN:def 2;
then rng BE is linearly-independent by VECTSP_7:def 3;
then A13: lines M is linearly-independent by ;
BE = M by A2, A7;
then M is one-to-one by MATRLIN:def 2;
then A14: the_rank_of M = n by ;
then Det M <> 0. F_Real by MATRIX13:83;
then A15: M is invertible by LAPLACE:34;
Mx2Tran M is onto by ;
then A16: rng () = the carrier of () by FUNCT_2:def 3;
A17: B c= () .: PP
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in B or x in () .: PP )
assume x in B ; :: thesis: x in () .: PP
then consider v being Element of () such that
A18: x = v and
A19: (v |-- E) | k in P by A9;
consider f being object such that
A20: ( f in dom () & () . f = v ) by ;
len (v |-- E) = n + 1 by ;
then len ((v |-- E) | n) = n by ;
then (v |-- E) | n is Element of n -tuples_on REAL by FINSEQ_2:92;
then (v |-- E) | n in n -tuples_on REAL ;
then (v |-- E) | n in REAL n by EUCLID:def 1;
then A21: (v |-- E) | n is Element of () by EUCLID:22;
reconsider w = v as Element of (Lin ()) by A2, A7, A3, A10, A4, A11, Th11;
A22: ((v |-- E) | n) | k = (v |-- E) | k by ;
f = w |-- BE by
.= (w |-- E) | ((card A) -' 1) by A8, A10, A12, Th24 ;
then f in PP by A2, A7, A19, A21, A22;
hence x in () .: PP by ; :: thesis: verum
end;
(Mx2Tran M) .: PP c= B
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in () .: PP or y in B )
assume y in () .: PP ; :: thesis: y in B
then consider x being object such that
x in dom () and
A23: x in PP and
A24: (Mx2Tran M) . x = y by FUNCT_1:def 6;
consider f being Element of () such that
A25: ( x = f & f | k in P ) by A23;
reconsider MTf = () . f as Element of (Lin ()) by A2, A7, A3, A10, A4, A11, Th11;
f = MTf |-- BE by
.= (MTf |-- E) | ((card A) -' 1) by A8, A10, A12, Th24 ;
then f | k = (MTf |-- E) | k by ;
hence y in B by A9, A24, A25; :: thesis: verum
end;
then A26: (Mx2Tran M) .: PP = B by A17;
( P is open iff PP is open ) by ;
hence ( P is open iff B is open ) by ; :: thesis: verum