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;

now :: thesis: for P being Subset of R^1 st P is closed holds
(|-- (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;

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