let x be set ; :: thesis: for n being Nat
for Affn being affinely-independent Subset of () st card Affn = n + 1 holds
|-- (Affn,x) is continuous

let n be Nat; :: thesis: for Affn being affinely-independent Subset of () st card Affn = n + 1 holds
|-- (Affn,x) is continuous

let Affn be affinely-independent Subset of (); :: 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 (() | (Affin Affn)),R^1 by Th31;
assume A1: card Affn = n + 1 ; :: thesis: |-- (Affn,x) is continuous
dim () = n by Th4;
then A2: Affin Affn = [#] () by ;
then A3: (TOP-REAL n) | (Affin Affn) = TopStruct(# the carrier of (), the topology of () #) by TSEP_1:93;
A4: dom (|-- (Affn,x)) = Affin Affn by ;
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 (), the topology of () #) by ;
(AxA " P) ` = ((|-- (Affn,x)) " P) ` by ;
then ((|-- (Affn,x)) " P) ` is open by ;
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