let x be set ; :: thesis: for n being Nat

for Affn being affinely-independent Subset of (TOP-REAL n) st card Affn = n + 1 holds

|-- (Affn,x) is continuous

let n be Nat; :: thesis: for Affn being affinely-independent Subset of (TOP-REAL n) st card Affn = n + 1 holds

|-- (Affn,x) is continuous

let Affn be affinely-independent Subset of (TOP-REAL n); :: thesis: ( card Affn = n + 1 implies |-- (Affn,x) is continuous )

set TRn = TOP-REAL n;

set AA = Affin Affn;

set Ax = |-- (Affn,x);

reconsider AxA = (|-- (Affn,x)) | (Affin Affn) as continuous Function of ((TOP-REAL n) | (Affin Affn)),R^1 by Th31;

assume A1: card Affn = n + 1 ; :: thesis: |-- (Affn,x) is continuous

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

then A2: Affin Affn = [#] (TOP-REAL n) by A1, Th6;

then A3: (TOP-REAL n) | (Affin Affn) = TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) by TSEP_1:93;

A4: dom (|-- (Affn,x)) = Affin Affn by A2, FUNCT_2:def 1;

for Affn being affinely-independent Subset of (TOP-REAL n) st card Affn = n + 1 holds

|-- (Affn,x) is continuous

let n be Nat; :: thesis: for Affn being affinely-independent Subset of (TOP-REAL n) st card Affn = n + 1 holds

|-- (Affn,x) is continuous

let Affn be affinely-independent Subset of (TOP-REAL n); :: thesis: ( card Affn = n + 1 implies |-- (Affn,x) is continuous )

set TRn = TOP-REAL n;

set AA = Affin Affn;

set Ax = |-- (Affn,x);

reconsider AxA = (|-- (Affn,x)) | (Affin Affn) as continuous Function of ((TOP-REAL n) | (Affin Affn)),R^1 by Th31;

assume A1: card Affn = n + 1 ; :: thesis: |-- (Affn,x) is continuous

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

then A2: Affin Affn = [#] (TOP-REAL n) by A1, Th6;

then A3: (TOP-REAL n) | (Affin Affn) = TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) by TSEP_1:93;

A4: dom (|-- (Affn,x)) = Affin Affn by A2, FUNCT_2:def 1;

now :: thesis: for P being Subset of R^1 st P is closed holds

(|-- (Affn,x)) " P is closed

hence
|-- (Affn,x) is continuous
by PRE_TOPC:def 6; :: thesis: verum(|-- (Affn,x)) " P is closed

let P be Subset of R^1; :: thesis: ( P is closed implies (|-- (Affn,x)) " P is closed )

assume P is closed ; :: thesis: (|-- (Affn,x)) " P is closed

then AxA " P is closed by PRE_TOPC:def 6;

then A5: (AxA " P) ` in the topology of TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) by A3, PRE_TOPC:def 2;

(AxA " P) ` = ((|-- (Affn,x)) " P) ` by A4, A3, RELAT_1:69;

then ((|-- (Affn,x)) " P) ` is open by A5, PRE_TOPC:def 2;

hence (|-- (Affn,x)) " P is closed by TOPS_1:3; :: thesis: verum

end;assume P is closed ; :: thesis: (|-- (Affn,x)) " P is closed

then AxA " P is closed by PRE_TOPC:def 6;

then A5: (AxA " P) ` in the topology of TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) by A3, PRE_TOPC:def 2;

(AxA " P) ` = ((|-- (Affn,x)) " P) ` by A4, A3, RELAT_1:69;

then ((|-- (Affn,x)) " P) ` is open by A5, PRE_TOPC:def 2;

hence (|-- (Affn,x)) " P is closed by TOPS_1:3; :: thesis: verum