let x be set ; :: thesis: for n being Nat
for Affn being affinely-independent Subset of () holds (|-- (Affn,x)) | (Affin Affn) is continuous Function of (() | (Affin Affn)),R^1

let n be Nat; :: thesis: for Affn being affinely-independent Subset of () holds (|-- (Affn,x)) | (Affin Affn) is continuous Function of (() | (Affin Affn)),R^1
let Affn be affinely-independent Subset of (); :: thesis: (|-- (Affn,x)) | (Affin Affn) is continuous Function of (() | (Affin Affn)),R^1
reconsider Z = 0 as Element of R^1 by ;
set TRn = TOP-REAL n;
set AA = Affin Affn;
set Ax = |-- (Affn,x);
set AxA = (|-- (Affn,x)) | (Affin Affn);
A1: ([#] ()) /\ (Affin Affn) = Affin Affn by XBOOLE_1:28;
A2: Affin Affn = [#] (() | (Affin Affn)) by PRE_TOPC:def 5;
then reconsider AxA = (|-- (Affn,x)) | (Affin Affn) as Function of (() | (Affin Affn)),R^1 by FUNCT_2:32;
A3: dom AxA = Affin Affn by ;
per cases ( not x in Affn or ( x in Affn & card Affn = 1 ) or ( x in Affn & card Affn <> 1 ) ) ;
suppose not x in Affn ; :: thesis: (|-- (Affn,x)) | (Affin Affn) is continuous Function of (() | (Affin Affn)),R^1
then |-- (Affn,x) = ([#] ()) --> Z by Th29;
then AxA = (() | (Affin Affn)) --> Z by ;
hence (|-- (Affn,x)) | (Affin Affn) is continuous Function of (() | (Affin Affn)),R^1 ; :: thesis: verum
end;
suppose A4: ( x in Affn & card Affn = 1 ) ; :: thesis: (|-- (Affn,x)) | (Affin Affn) is continuous Function of (() | (Affin Affn)),R^1
A5: rng AxA c= the carrier of R^1 by RELAT_1:def 19;
consider y being object such that
A6: Affn = {y} by ;
A7: x = y by ;
then Affn is Affine by ;
then A8: Affin Affn = Affn by RLAFFIN1:50;
then AxA . x in rng AxA by ;
then reconsider b = AxA . x as Element of R^1 by A5;
rng AxA = {(AxA . x)} by ;
then AxA = (() | (Affin Affn)) --> b by ;
hence (|-- (Affn,x)) | (Affin Affn) is continuous Function of (() | (Affin Affn)),R^1 ; :: thesis: verum
end;
suppose A9: ( x in Affn & card Affn <> 1 ) ; :: thesis: (|-- (Affn,x)) | (Affin Affn) is continuous Function of (() | (Affin Affn)),R^1
set P2 = the Enumeration of Affn \ {x};
set P1 = <*x*>;
set P12 = <*x*> ^ the Enumeration of Affn \ {x};
A10: ( rng <*x*> = {x} & rng the Enumeration of Affn \ {x} = Affn \ {x} ) by ;
( <*x*> is one-to-one & {x} misses Affn \ {x} ) by ;
then A11: <*x*> ^ the Enumeration of Affn \ {x} is one-to-one by ;
rng (<*x*> ^ the Enumeration of Affn \ {x}) = () \/ (rng the Enumeration of Affn \ {x}) by FINSEQ_1:31;
then rng (<*x*> ^ the Enumeration of Affn \ {x}) = Affn by ;
then reconsider P12 = <*x*> ^ the Enumeration of Affn \ {x} as Enumeration of Affn by ;
set TR1 = TOP-REAL 1;
consider Pro being Function of (),R^1 such that
A12: for p being Element of () holds Pro . p = p /. 1 by JORDAN2B:1;
A13: Pro is being_homeomorphism by ;
card Affn >= 1 by ;
then A14: card Affn > 1 by ;
now :: thesis: for P being Subset of R^1 st P is closed holds
AxA " P is closed
A15: dom <*x*> c= dom P12 by FINSEQ_1:26;
let P be Subset of R^1; :: thesis: ( P is closed implies AxA " P is closed )
set B = { v where v is Element of (() | (Affin Affn)) : (v |-- P12) | 1 in Pro " P } ;
A16: 1 in {1} by FINSEQ_1:2;
assume P is closed ; :: thesis: AxA " P is closed
then A17: Pro " P is closed by ;
A18: dom <*x*> = Seg 1 by FINSEQ_1:38;
then A19: P12 . 1 = <*x*> . 1 by
.= x by FINSEQ_1:40 ;
A20: not Affin Affn is empty by A9;
A21: { v where v is Element of (() | (Affin Affn)) : (v |-- P12) | 1 in Pro " P } c= AxA " P
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { v where v is Element of (() | (Affin Affn)) : (v |-- P12) | 1 in Pro " P } or y in AxA " P )
assume y in { v where v is Element of (() | (Affin Affn)) : (v |-- P12) | 1 in Pro " P } ; :: thesis: y in AxA " P
then consider v being Element of (() | (Affin Affn)) such that
A22: y = v and
A23: (v |-- P12) | 1 in Pro " P ;
set vP = v |-- P12;
reconsider vP1 = (v |-- P12) | 1 as Element of () by A23;
A24: v in Affin Affn by ;
len vP1 = 1 by CARD_1:def 7;
then dom vP1 = Seg 1 by FINSEQ_1:def 3;
then A25: 1 in dom vP1 ;
then A26: 1 in dom (v |-- P12) by RELAT_1:57;
Pro . vP1 = vP1 /. 1 by A12
.= vP1 . 1 by
.= (v |-- P12) . 1 by
.= (v |-- Affn) . x by
.= (|-- (Affn,x)) . v by ;
then (|-- (Affn,x)) . v in P by ;
then AxA . v in P by ;
hence y in AxA " P by ; :: thesis: verum
end;
A27: dom Pro = [#] () by ;
AxA " P c= { v where v is Element of (() | (Affin Affn)) : (v |-- P12) | 1 in Pro " P }
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in AxA " P or y in { v where v is Element of (() | (Affin Affn)) : (v |-- P12) | 1 in Pro " P } )
set yP = y |-- P12;
len (y |-- P12) = card Affn by Th16;
then A28: len ((y |-- P12) | 1) = 1 by ;
then reconsider yP1 = (y |-- P12) | 1 as Element of () by TOPREAL3:46;
A29: dom yP1 = Seg 1 by ;
assume A30: y in AxA " P ; :: thesis: y in { v where v is Element of (() | (Affin Affn)) : (v |-- P12) | 1 in Pro " P }
then A31: y in dom AxA by FUNCT_1:def 7;
then AxA . y = (|-- (Affn,x)) . y by FUNCT_1:47
.= (y |-- Affn) . (P12 . 1) by A19, A3, A31, Def3
.= (y |-- P12) . 1 by
.= yP1 . 1 by
.= yP1 /. 1 by
.= Pro . yP1 by A12 ;
then Pro . yP1 in P by ;
then yP1 in Pro " P by ;
hence y in { v where v is Element of (() | (Affin Affn)) : (v |-- P12) | 1 in Pro " P } by A30; :: thesis: verum
end;
then { v where v is Element of (() | (Affin Affn)) : (v |-- P12) | 1 in Pro " P } = AxA " P by A21;
hence AxA " P is closed by ; :: thesis: verum
end;
hence (|-- (Affn,x)) | (Affin Affn) is continuous Function of (() | (Affin Affn)),R^1 by PRE_TOPC:def 6; :: thesis: verum
end;
end;