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

for Affn being affinely-independent Subset of (TOP-REAL n) holds (|-- (Affn,x)) | (Affin Affn) is continuous Function of ((TOP-REAL n) | (Affin Affn)),R^1

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

let Affn be affinely-independent Subset of (TOP-REAL n); :: thesis: (|-- (Affn,x)) | (Affin Affn) is continuous Function of ((TOP-REAL n) | (Affin Affn)),R^1

reconsider Z = 0 as Element of R^1 by Lm5, TOPMETR:17;

set TRn = TOP-REAL n;

set AA = Affin Affn;

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

set AxA = (|-- (Affn,x)) | (Affin Affn);

A1: ([#] (TOP-REAL n)) /\ (Affin Affn) = Affin Affn by XBOOLE_1:28;

A2: Affin Affn = [#] ((TOP-REAL n) | (Affin Affn)) by PRE_TOPC:def 5;

then reconsider AxA = (|-- (Affn,x)) | (Affin Affn) as Function of ((TOP-REAL n) | (Affin Affn)),R^1 by FUNCT_2:32;

A3: dom AxA = Affin Affn by A2, FUNCT_2:def 1;

for Affn being affinely-independent Subset of (TOP-REAL n) holds (|-- (Affn,x)) | (Affin Affn) is continuous Function of ((TOP-REAL n) | (Affin Affn)),R^1

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

let Affn be affinely-independent Subset of (TOP-REAL n); :: thesis: (|-- (Affn,x)) | (Affin Affn) is continuous Function of ((TOP-REAL n) | (Affin Affn)),R^1

reconsider Z = 0 as Element of R^1 by Lm5, TOPMETR:17;

set TRn = TOP-REAL n;

set AA = Affin Affn;

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

set AxA = (|-- (Affn,x)) | (Affin Affn);

A1: ([#] (TOP-REAL n)) /\ (Affin Affn) = Affin Affn by XBOOLE_1:28;

A2: Affin Affn = [#] ((TOP-REAL n) | (Affin Affn)) by PRE_TOPC:def 5;

then reconsider AxA = (|-- (Affn,x)) | (Affin Affn) as Function of ((TOP-REAL n) | (Affin Affn)),R^1 by FUNCT_2:32;

A3: dom AxA = Affin Affn by A2, FUNCT_2:def 1;

per cases
( not x in Affn or ( x in Affn & card Affn = 1 ) or ( x in Affn & card Affn <> 1 ) )
;

end;

suppose
not x in Affn
; :: thesis: (|-- (Affn,x)) | (Affin Affn) is continuous Function of ((TOP-REAL n) | (Affin Affn)),R^1

then
|-- (Affn,x) = ([#] (TOP-REAL n)) --> Z
by Th29;

then AxA = ((TOP-REAL n) | (Affin Affn)) --> Z by A2, A1, FUNCOP_1:12;

hence (|-- (Affn,x)) | (Affin Affn) is continuous Function of ((TOP-REAL n) | (Affin Affn)),R^1 ; :: thesis: verum

end;then AxA = ((TOP-REAL n) | (Affin Affn)) --> Z by A2, A1, FUNCOP_1:12;

hence (|-- (Affn,x)) | (Affin Affn) is continuous Function of ((TOP-REAL n) | (Affin Affn)),R^1 ; :: thesis: verum

suppose A4:
( x in Affn & card Affn = 1 )
; :: thesis: (|-- (Affn,x)) | (Affin Affn) is continuous Function of ((TOP-REAL n) | (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 A4, CARD_2:42;

A7: x = y by A4, A6, TARSKI:def 1;

then Affn is Affine by A4, A6, RUSUB_4:23;

then A8: Affin Affn = Affn by RLAFFIN1:50;

then AxA . x in rng AxA by A3, A4, FUNCT_1:def 3;

then reconsider b = AxA . x as Element of R^1 by A5;

rng AxA = {(AxA . x)} by A3, A6, A7, A8, FUNCT_1:4;

then AxA = ((TOP-REAL n) | (Affin Affn)) --> b by A2, A3, FUNCOP_1:9;

hence (|-- (Affn,x)) | (Affin Affn) is continuous Function of ((TOP-REAL n) | (Affin Affn)),R^1 ; :: thesis: verum

end;consider y being object such that

A6: Affn = {y} by A4, CARD_2:42;

A7: x = y by A4, A6, TARSKI:def 1;

then Affn is Affine by A4, A6, RUSUB_4:23;

then A8: Affin Affn = Affn by RLAFFIN1:50;

then AxA . x in rng AxA by A3, A4, FUNCT_1:def 3;

then reconsider b = AxA . x as Element of R^1 by A5;

rng AxA = {(AxA . x)} by A3, A6, A7, A8, FUNCT_1:4;

then AxA = ((TOP-REAL n) | (Affin Affn)) --> b by A2, A3, FUNCOP_1:9;

hence (|-- (Affn,x)) | (Affin Affn) is continuous Function of ((TOP-REAL n) | (Affin Affn)),R^1 ; :: thesis: verum

suppose A9:
( x in Affn & card Affn <> 1 )
; :: thesis: (|-- (Affn,x)) | (Affin Affn) is continuous Function of ((TOP-REAL n) | (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 Def1, FINSEQ_1:39;

( <*x*> is one-to-one & {x} misses Affn \ {x} ) by FINSEQ_3:93, XBOOLE_1:79;

then A11: <*x*> ^ the Enumeration of Affn \ {x} is one-to-one by A10, FINSEQ_3:91;

rng (<*x*> ^ the Enumeration of Affn \ {x}) = (rng <*x*>) \/ (rng the Enumeration of Affn \ {x}) by FINSEQ_1:31;

then rng (<*x*> ^ the Enumeration of Affn \ {x}) = Affn by A9, A10, ZFMISC_1:116;

then reconsider P12 = <*x*> ^ the Enumeration of Affn \ {x} as Enumeration of Affn by A11, Def1;

set TR1 = TOP-REAL 1;

consider Pro being Function of (TOP-REAL 1),R^1 such that

A12: for p being Element of (TOP-REAL 1) holds Pro . p = p /. 1 by JORDAN2B:1;

A13: Pro is being_homeomorphism by A12, JORDAN2B:28;

card Affn >= 1 by A9, NAT_1:14;

then A14: card Affn > 1 by A9, XXREAL_0:1;

end;set P1 = <*x*>;

set P12 = <*x*> ^ the Enumeration of Affn \ {x};

A10: ( rng <*x*> = {x} & rng the Enumeration of Affn \ {x} = Affn \ {x} ) by Def1, FINSEQ_1:39;

( <*x*> is one-to-one & {x} misses Affn \ {x} ) by FINSEQ_3:93, XBOOLE_1:79;

then A11: <*x*> ^ the Enumeration of Affn \ {x} is one-to-one by A10, FINSEQ_3:91;

rng (<*x*> ^ the Enumeration of Affn \ {x}) = (rng <*x*>) \/ (rng the Enumeration of Affn \ {x}) by FINSEQ_1:31;

then rng (<*x*> ^ the Enumeration of Affn \ {x}) = Affn by A9, A10, ZFMISC_1:116;

then reconsider P12 = <*x*> ^ the Enumeration of Affn \ {x} as Enumeration of Affn by A11, Def1;

set TR1 = TOP-REAL 1;

consider Pro being Function of (TOP-REAL 1),R^1 such that

A12: for p being Element of (TOP-REAL 1) holds Pro . p = p /. 1 by JORDAN2B:1;

A13: Pro is being_homeomorphism by A12, JORDAN2B:28;

card Affn >= 1 by A9, NAT_1:14;

then A14: card Affn > 1 by A9, XXREAL_0:1;

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

AxA " P is closed

hence
(|-- (Affn,x)) | (Affin Affn) is continuous Function of ((TOP-REAL n) | (Affin Affn)),R^1
by PRE_TOPC:def 6; :: thesis: verumAxA " 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 ((TOP-REAL n) | (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 A13, TOPGRP_1:24;

A18: dom <*x*> = Seg 1 by FINSEQ_1:38;

then A19: P12 . 1 = <*x*> . 1 by A16, FINSEQ_1:2, FINSEQ_1:def 7

.= x by FINSEQ_1:40 ;

A20: not Affin Affn is empty by A9;

A21: { v where v is Element of ((TOP-REAL n) | (Affin Affn)) : (v |-- P12) | 1 in Pro " P } c= AxA " P

AxA " P c= { v where v is Element of ((TOP-REAL n) | (Affin Affn)) : (v |-- P12) | 1 in Pro " P }

hence AxA " P is closed by A14, A17, Th28; :: thesis: verum

end;let P be Subset of R^1; :: thesis: ( P is closed implies AxA " P is closed )

set B = { v where v is Element of ((TOP-REAL n) | (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 A13, TOPGRP_1:24;

A18: dom <*x*> = Seg 1 by FINSEQ_1:38;

then A19: P12 . 1 = <*x*> . 1 by A16, FINSEQ_1:2, FINSEQ_1:def 7

.= x by FINSEQ_1:40 ;

A20: not Affin Affn is empty by A9;

A21: { v where v is Element of ((TOP-REAL n) | (Affin Affn)) : (v |-- P12) | 1 in Pro " P } c= AxA " P

proof

A27:
dom Pro = [#] (TOP-REAL 1)
by A13, TOPGRP_1:24;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { v where v is Element of ((TOP-REAL n) | (Affin Affn)) : (v |-- P12) | 1 in Pro " P } or y in AxA " P )

assume y in { v where v is Element of ((TOP-REAL n) | (Affin Affn)) : (v |-- P12) | 1 in Pro " P } ; :: thesis: y in AxA " P

then consider v being Element of ((TOP-REAL n) | (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 (TOP-REAL 1) by A23;

A24: v in Affin Affn by A2, A20;

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 A25, PARTFUN1:def 6

.= (v |-- P12) . 1 by A25, FUNCT_1:47

.= (v |-- Affn) . x by A19, A26, FUNCT_1:12

.= (|-- (Affn,x)) . v by A24, Def3 ;

then (|-- (Affn,x)) . v in P by A23, FUNCT_1:def 7;

then AxA . v in P by A2, A3, A9, FUNCT_1:47;

hence y in AxA " P by A2, A3, A9, A22, FUNCT_1:def 7; :: thesis: verum

end;assume y in { v where v is Element of ((TOP-REAL n) | (Affin Affn)) : (v |-- P12) | 1 in Pro " P } ; :: thesis: y in AxA " P

then consider v being Element of ((TOP-REAL n) | (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 (TOP-REAL 1) by A23;

A24: v in Affin Affn by A2, A20;

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 A25, PARTFUN1:def 6

.= (v |-- P12) . 1 by A25, FUNCT_1:47

.= (v |-- Affn) . x by A19, A26, FUNCT_1:12

.= (|-- (Affn,x)) . v by A24, Def3 ;

then (|-- (Affn,x)) . v in P by A23, FUNCT_1:def 7;

then AxA . v in P by A2, A3, A9, FUNCT_1:47;

hence y in AxA " P by A2, A3, A9, A22, FUNCT_1:def 7; :: thesis: verum

AxA " P c= { v where v is Element of ((TOP-REAL n) | (Affin Affn)) : (v |-- P12) | 1 in Pro " P }

proof

then
{ v where v is Element of ((TOP-REAL n) | (Affin Affn)) : (v |-- P12) | 1 in Pro " P } = AxA " P
by A21;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in AxA " P or y in { v where v is Element of ((TOP-REAL n) | (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 A9, FINSEQ_1:59, NAT_1:14;

then reconsider yP1 = (y |-- P12) | 1 as Element of (TOP-REAL 1) by TOPREAL3:46;

A29: dom yP1 = Seg 1 by A28, FINSEQ_1:def 3;

assume A30: y in AxA " P ; :: thesis: y in { v where v is Element of ((TOP-REAL n) | (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 A18, A16, A15, FINSEQ_1:2, FUNCT_1:13

.= yP1 . 1 by A16, A29, FINSEQ_1:2, FUNCT_1:47

.= yP1 /. 1 by A16, A29, FINSEQ_1:2, PARTFUN1:def 6

.= Pro . yP1 by A12 ;

then Pro . yP1 in P by A30, FUNCT_1:def 7;

then yP1 in Pro " P by A27, FUNCT_1:def 7;

hence y in { v where v is Element of ((TOP-REAL n) | (Affin Affn)) : (v |-- P12) | 1 in Pro " P } by A30; :: thesis: verum

end;set yP = y |-- P12;

len (y |-- P12) = card Affn by Th16;

then A28: len ((y |-- P12) | 1) = 1 by A9, FINSEQ_1:59, NAT_1:14;

then reconsider yP1 = (y |-- P12) | 1 as Element of (TOP-REAL 1) by TOPREAL3:46;

A29: dom yP1 = Seg 1 by A28, FINSEQ_1:def 3;

assume A30: y in AxA " P ; :: thesis: y in { v where v is Element of ((TOP-REAL n) | (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 A18, A16, A15, FINSEQ_1:2, FUNCT_1:13

.= yP1 . 1 by A16, A29, FINSEQ_1:2, FUNCT_1:47

.= yP1 /. 1 by A16, A29, FINSEQ_1:2, PARTFUN1:def 6

.= Pro . yP1 by A12 ;

then Pro . yP1 in P by A30, FUNCT_1:def 7;

then yP1 in Pro " P by A27, FUNCT_1:def 7;

hence y in { v where v is Element of ((TOP-REAL n) | (Affin Affn)) : (v |-- P12) | 1 in Pro " P } by A30; :: thesis: verum

hence AxA " P is closed by A14, A17, Th28; :: thesis: verum