let n be Nat; :: thesis:
let p0 be Point of (TOP-REAL (n + 1)); :: thesis:
assume A1: p0 = Base_FinSeq ((n + 1),(n + 1)) ; :: thesis:
set T = TOP-REAL n;
set S = TPlane (p0,(0. (TOP-REAL (n + 1))));
defpred S₁[ set , set ] means for p being Element of (TOP-REAL n) st $1 = p holds
$2 = p ^ <*0*>;
A2: for p being Element of (TOP-REAL n) holds p ^ <*0*> is Element of (TPlane (p0,(0. (TOP-REAL (n + 1)))))

proof

let p be Element of (TOP-REAL n); :: thesis:
A3: len p = n by CARD_1:def 7;
A4: len (p ^ <*0*>) = n + 1 by CARD_1:def 7;
rng (p ^ <*0*>) c= REAL ;
then p ^ <*0*> in REAL (n + 1) by A4, FINSEQ_2:132;
then reconsider q = p ^ <*0*> as Point of (TOP-REAL (n + 1)) by EUCLID:22;
reconsider r0 = 0 as Real ;
( dom p0 = Seg (n + 1) & dom q = Seg (n + 1) ) by FINSEQ_1:89;
then (dom p0) /\ (dom q) = Seg (n + 1) ;
then A5: dom (mlt (p0,q)) = Seg (n + 1) by VALUED_1:def 4;
for y being object holds
( y in rng (mlt (p0,q)) iff y = r0 )

proof

let y be object ; :: thesis:
set f = mlt (p0,q);

A6: now :: thesis:

let x be set ; :: thesis:
assume x in Seg (n + 1) ; :: thesis:
then consider k being Nat such that
A7: ( x = k & 1 <= k & k <= n + 1 ) ;
A8: (mlt (p0,q)) . x = (p0 . x) * (q . x) by VALUED_1:5;

per cases ;

suppose A9: k = n + 1 ; :: thesis:

1 <= len <*r0*> by FINSEQ_1:39;
then q . ((len p) + 1) = <*r0*> . 1 by FINSEQ_1:65
.= r0 by FINSEQ_1:40 ;
hence (mlt (p0,q)) . x = r0 by A8, A7, A9, A3; :: thesis:

end;

suppose k <> n + 1 ; :: thesis:

then p0 . x = 0 by A1, A7, MATRIXR2:76;
hence (mlt (p0,q)) . x = r0 by A8; :: thesis:

end;

hereby :: thesis:

assume y in rng (mlt (p0,q)) ; :: thesis:
then consider x being object such that
A10: ( x in dom (mlt (p0,q)) & y = (mlt (p0,q)) . x ) by FUNCT_1:def 3;
thus y = r0 by A10, A5, A6; :: thesis:

end;

assume A11: y = r0 ; :: thesis:
consider x being object such that
A12: x in Seg (n + 1) by XBOOLE_0:def 1;
y = (mlt (p0,q)) . x by A11, A12, A6;
hence y in rng (mlt (p0,q)) by A12, A5, FUNCT_1:def 3; :: thesis:

end;

then mlt (p0,q) = (Seg (n + 1)) --> r0 by A5, FUNCOP_1:9, TARSKI:def 1;
then A14: mlt (p0,q) = (n + 1) |-> r0 by FINSEQ_2:def 2;
A15: |(p0,q)| = Sum (mlt (p0,q)) by RVSUM_1:def 16
.= (n + 1) * r0 by A14, RVSUM_1:80
.= 0 ;
|(p0,(q - (0. (TOP-REAL (n + 1)))))| = |(p0,q)| - |(p0,(0. (TOP-REAL (n + 1))))| by EUCLID_2:27
.= |(p0,q)| - 0 by EUCLID_2:32
.= 0 by A15 ;
then p ^ <*0*> in Plane (p0,(0. (TOP-REAL (n + 1)))) ;
then p ^ <*0*> in [#] (TPlane (p0,(0. (TOP-REAL (n + 1))))) by PRE_TOPC:def 5;
hence p ^ <*0*> is Element of (TPlane (p0,(0. (TOP-REAL (n + 1))))) ; :: thesis:

end;

A16: for x being Element of (TOP-REAL n) ex y being Element of (TPlane (p0,(0. (TOP-REAL (n + 1))))) st S₁[x,y]

proof

let x be Element of (TOP-REAL n); :: thesis:
set y = x ^ <*0*>;
reconsider y = x ^ <*0*> as Element of (TPlane (p0,(0. (TOP-REAL (n + 1))))) by A2;
take y ; :: thesis:
thus S₁[x,y] ; :: thesis:

end;

consider f being Function of (TOP-REAL n),(TPlane (p0,(0. (TOP-REAL (n + 1))))) such that
A17: for x being Element of (TOP-REAL n) holds S₁[x,f . x] from FUNCT_2:sch 3(A16);
A18: dom f = [#] (TOP-REAL n) by FUNCT_2:def 1;
A19: for y being object holds
( y in [#] (TPlane (p0,(0. (TOP-REAL (n + 1))))) iff ex x being object st
( x in dom f & y = f . x ) )

proof

let y be object ; :: thesis:

hereby :: thesis:

assume y in [#] (TPlane (p0,(0. (TOP-REAL (n + 1))))) ; :: thesis:
then y in Plane (p0,(0. (TOP-REAL (n + 1)))) by PRE_TOPC:def 5;
then consider q being Point of (TOP-REAL (n + 1)) such that
A20: ( y = q & |(p0,(q - (0. (TOP-REAL (n + 1)))))| = 0 ) ;
A21: ( len q = n + 1 & rng q c= REAL ) by CARD_1:def 7;
then reconsider q1 = q as FinSequence of REAL by FINSEQ_1:def 4;
set p = q1 | n;
reconsider x = q1 | n as object ;
take x = x; :: thesis:
0 + n <= 1 + n by XREAL_1:6;
then A22: len (q1 | n) = n by A21, FINSEQ_1:59;
A23: rng (q1 | n) c= REAL ;
A24: q1 | n in REAL n by A22, A23, FINSEQ_2:132;
hence x in dom f by A18, EUCLID:22; :: thesis:
reconsider x1 = x as Element of (TOP-REAL n) by A24, EUCLID:22;
S₁[x1,f . x1] by A17;
then A25: f . x = (q1 | n) ^ <*0*> ;
A26: q = (q1 | n) ^ <*(q . (n + 1))*> by CARD_1:def 7, FINSEQ_3:55;
A27: |(p0,(q - (0. (TOP-REAL (n + 1)))))| = |(p0,q)| - |(p0,(0. (TOP-REAL (n + 1))))| by EUCLID_2:27
.= |(p0,q)| - 0 by EUCLID_2:32
.= |(p0,q)| ;
reconsider f0 = 0. (TOP-REAL n) as FinSequence of REAL by EUCLID:24;
rng <*1*> c= REAL ;
then reconsider f1 = <*1*> as FinSequence of REAL by FINSEQ_1:def 4;
reconsider f3 = <*(q . (n + 1))*> as FinSequence of REAL by RVSUM_1:145;
q1 | n in REAL n by A22, A23, FINSEQ_2:132;
then reconsider p1 = q1 | n as Point of (TOP-REAL n) by EUCLID:22;
A28: |((f0 ^ f1),((q1 | n) ^ f3))| = 0 by A1, A26, A27, A20, Th28;
reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
0. (TOP-REAL n) in the carrier of (TOP-REAL n) ;
then f0 in REAL n by EUCLID:22;
then f0 in Funcs ((Seg n1),REAL) by FINSEQ_2:93;
then consider g being Function such that
A29: ( f0 = g & dom g = Seg n1 & rng g c= REAL ) by FUNCT_2:def 2;
A30: len f0 = len (q1 | n) by A22, A29, FINSEQ_1:def 3;
len f1 = 1 by FINSEQ_1:39
.= len f3 by FINSEQ_1:39 ;
then |((0. (TOP-REAL n)),p1)| + |(f1,f3)| = 0 by A28, A30, Th15;
then 0 + |(f1,f3)| = 0 by EUCLID_2:33;
then Sum (mlt (f1,f3)) = 0 by RVSUM_1:def 16;
then Sum <*(1 * (q . (n + 1)))*> = 0 by RVSUM_1:62;
hence y = f . x by A20, A25, A26, RVSUM_1:73; :: thesis:

end;

given x being object such that A31: ( x in dom f & y = f . x ) ; :: thesis:
reconsider p = x as Element of (TOP-REAL n) by A31;
S₁[p,f . p] by A17;
hence y in [#] (TPlane (p0,(0. (TOP-REAL (n + 1))))) by A31; :: thesis:

end;

then A32: rng f = [#] (TPlane (p0,(0. (TOP-REAL (n + 1))))) by FUNCT_1:def 3;
for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2

proof

let x1, x2 be object ; :: thesis:
assume A33: ( x1 in dom f & x2 in dom f ) ; :: thesis:
assume A34: f . x1 = f . x2 ; :: thesis:
reconsider p1 = x1, p2 = x2 as Element of (TOP-REAL n) by A33;
( f . p1 = p1 ^ <*0*> & f . p2 = p2 ^ <*0*> ) by A17;
hence x1 = x2 by A34, FINSEQ_1:33; :: thesis:

end;

then A35: f is one-to-one ;
set T1 = TOP-REAL (n + 1);
A36: for p1 being Point of (TOP-REAL n) holds f . p1 is Point of (TOP-REAL (n + 1))

proof

let p1 be Point of (TOP-REAL n); :: thesis:
[#] (TPlane (p0,(0. (TOP-REAL (n + 1))))) c= [#] (TOP-REAL (n + 1)) by PRE_TOPC:def 4;
hence f . p1 is Point of (TOP-REAL (n + 1)) ; :: thesis:

end;

A37: for p1 being Point of (TOP-REAL n)
for q1 being Point of (TOP-REAL (n + 1)) st q1 = f . p1 holds
|.p1.| = |.q1.|

proof

let p1 be Point of (TOP-REAL n); :: thesis:
let q1 be Point of (TOP-REAL (n + 1)); :: thesis:
assume q1 = f . p1 ; :: thesis:
then A38: q1 = p1 ^ <*0*> by A17;
reconsider x = q1 as Element of REAL (n + 1) by EUCLID:22;
A39: ( len p1 = n & rng p1 c= REAL ) by CARD_1:def 7;
A40: x | n = (p1 ^ <*0*>) | (dom p1) by A38, FINSEQ_1:89
.= p1 by FINSEQ_1:21 ;
A41: x . (n + 1) = 0 by A38, A39, FINSEQ_1:42;
A42: |.q1.| ^2 = (|.p1.| ^2) + (0 ^2) by A40, A41, REAL_NS1:10
.= (|.p1.| ^2) + (0 * 0) by SQUARE_1:def 1
.= |.p1.| ^2 ;
|.q1.| * |.q1.| >= 0 ;
then A43: |.q1.| ^2 >= 0 by SQUARE_1:def 1;
|.p1.| * |.p1.| >= 0 ;
then |.p1.| ^2 >= 0 by SQUARE_1:def 1;
hence |.p1.| = sqrt (|.q1.| ^2) by A42, SQUARE_1:def 2
.= |.q1.| by A43, SQUARE_1:def 2 ;
:: thesis:

end;

A44: for p1, p2 being Point of (TOP-REAL n)
for q1, q2 being Point of (TOP-REAL (n + 1)) st q1 = f . p1 & q2 = f . p2 holds
f . (p1 - p2) = q1 - q2

proof

let p1, p2 be Point of (TOP-REAL n); :: thesis:
let q1, q2 be Point of (TOP-REAL (n + 1)); :: thesis:
assume q1 = f . p1 ; :: thesis:
then A45: q1 = p1 ^ <*0*> by A17;
assume q2 = f . p2 ; :: thesis:
then A46: q2 = p2 ^ <*0*> by A17;
A47: f . (p1 - p2) = (p1 - p2) ^ <*0*> by A17;
reconsider qa = f . (p1 - p2) as Point of (TOP-REAL (n + 1)) by A36;
A48: dom ((p1 - p2) ^ <*0*>) = Seg (n + 1) by FINSEQ_1:89
.= dom (q1 - q2) by FINSEQ_1:89 ;
for k being Nat st k in dom (q1 - q2) holds
(q1 - q2) . k = ((p1 - p2) ^ <*0*>) . k

proof

let k be Nat; :: thesis:
assume k in dom (q1 - q2) ; :: thesis:
then A49: k in Seg (n + 1) by FINSEQ_1:89;
A50: (q1 - q2) . k = (q1 . k) + ((- q2) . k) by A49, Th16
.= (q1 . k) + (((- 1) * q2) . k) by RLVECT_1:16
.= (q1 . k) + ((- 1) * (q2 . k)) by VALUED_1:6 ;
A51: k in (Seg n) \/ {(n + 1)} by A49, FINSEQ_1:9;

per cases by A51, XBOOLE_0:def 3;

suppose A52: k in Seg n ; :: thesis:

then ( k in dom p1 & k in dom p2 ) by FINSEQ_1:89;
then A53: ( q1 . k = p1 . k & q2 . k = p2 . k ) by A45, A46, FINSEQ_1:def 7;
k in dom (p1 - p2) by A52, FINSEQ_1:89;
then ((p1 - p2) ^ <*0*>) . k = (p1 - p2) . k by FINSEQ_1:def 7
.= (p1 . k) + ((- p2) . k) by A52, Th16
.= (p1 . k) + (((- 1) * p2) . k) by RLVECT_1:16
.= (p1 . k) + ((- 1) * (p2 . k)) by VALUED_1:6 ;
hence (q1 - q2) . k = ((p1 - p2) ^ <*0*>) . k by A50, A53; :: thesis:

end;

suppose k in {(n + 1)} ; :: thesis:

then A54: k = n + 1 by TARSKI:def 1;
( len p1 = n & len p2 = n ) by CARD_1:def 7;
then A55: ( q1 . k = 0 & q2 . k = 0 ) by A45, A46, A54, FINSEQ_1:42;
len (p1 - p2) = n by CARD_1:def 7;
hence (q1 - q2) . k = ((p1 - p2) ^ <*0*>) . k by A50, A55, A54, FINSEQ_1:42; :: thesis:

end;

hence f . (p1 - p2) = q1 - q2 by A47, A48, FINSEQ_1:13; :: thesis:

end;

A56: f .: ([#] (TOP-REAL n)) = [#] (TPlane (p0,(0. (TOP-REAL (n + 1))))) by A32, RELSET_1:22;
for P being Subset of (TOP-REAL n) holds
( P is closed iff f .: P is closed )

proof

let P be Subset of (TOP-REAL n); :: thesis:

hereby :: thesis:

assume P is closed ; :: thesis:
then A57: ([#] (TOP-REAL n)) \ P in the topology of (TOP-REAL n) by PRE_TOPC:def 2, PRE_TOPC:def 3;
set FQ = { (Ball (q,r)) where q is Point of (TOP-REAL (n + 1)), r is Real : ex p being Point of (TOP-REAL n) st
( q = f . p & Ball (p,r) c= ([#] (TOP-REAL n)) \ P ) } ;
for x being object st x in { (Ball (q,r)) where q is Point of (TOP-REAL (n + 1)), r is Real : ex p being Point of (TOP-REAL n) st
( q = f . p & Ball (p,r) c= ([#] (TOP-REAL n)) \ P ) } holds
x in bool ([#] (TOP-REAL (n + 1)))

proof

let x be object ; :: thesis:
assume x in { (Ball (q,r)) where q is Point of (TOP-REAL (n + 1)), r is Real : ex p being Point of (TOP-REAL n) st
( q = f . p & Ball (p,r) c= ([#] (TOP-REAL n)) \ P ) } ; :: thesis:
then consider q being Point of (TOP-REAL (n + 1)), r being Real such that
A58: ( x = Ball (q,r) & ex p being Point of (TOP-REAL n) st
( q = f . p & Ball (p,r) c= ([#] (TOP-REAL n)) \ P ) ) ;
thus x in bool ([#] (TOP-REAL (n + 1))) by A58; :: thesis:

end;

then reconsider FQ = { (Ball (q,r)) where q is Point of (TOP-REAL (n + 1)), r is Real : ex p being Point of (TOP-REAL n) st
( q = f . p & Ball (p,r) c= ([#] (TOP-REAL n)) \ P ) } as Subset-Family of (TOP-REAL (n + 1)) by TARSKI:def 3;
B60: for Q being Subset of (TOP-REAL (n + 1)) st Q in FQ holds
Q is open

proof

let Q be Subset of (TOP-REAL (n + 1)); :: thesis:
assume Q in FQ ; :: thesis:
then consider q being Point of (TOP-REAL (n + 1)), r being Real such that
A59: ( Q = Ball (q,r) & ex p being Point of (TOP-REAL n) st
( q = f . p & Ball (p,r) c= ([#] (TOP-REAL n)) \ P ) ) ;
thus Q is open by A59; :: thesis:

end;

set Q = union FQ;
union FQ is open by B60, TOPS_2:def 1, TOPS_2:19;
then A61: union FQ in the topology of (TOP-REAL (n + 1)) by PRE_TOPC:def 2;
for y being Element of (TPlane (p0,(0. (TOP-REAL (n + 1))))) holds
( y in f .: (([#] (TOP-REAL n)) \ P) iff y in (union FQ) /\ ([#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))) )

proof

let y be Element of (TPlane (p0,(0. (TOP-REAL (n + 1))))); :: thesis:

hereby :: thesis:

assume y in f .: (([#] (TOP-REAL n)) \ P) ; :: thesis:
then consider x being object such that
A62: ( x in dom f & x in ([#] (TOP-REAL n)) \ P & y = f . x ) by FUNCT_1:def 6;
reconsider p = x as Point of (TOP-REAL n) by A62;
reconsider q = y as Point of (TOP-REAL (n + 1)) by A62, A36;
consider r being Real such that
A63: ( r > 0 & Ball (p,r) c= ([#] (TOP-REAL n)) \ P ) by A62, A57, Th24;
A64: Ball (q,r) in FQ by A62, A63;
q in Ball (q,r) by A63, JORDAN:16;
then y in union FQ by A64, TARSKI:def 4;
hence y in (union FQ) /\ ([#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))) by XBOOLE_0:def 4; :: thesis:

end;

assume y in (union FQ) /\ ([#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))) ; :: thesis:
then y in union FQ by XBOOLE_0:def 4;
then consider Y being set such that
A65: ( y in Y & Y in FQ ) by TARSKI:def 4;
consider q being Point of (TOP-REAL (n + 1)), r being Real such that
A66: Y = Ball (q,r) and
A67: ex p being Point of (TOP-REAL n) st
( q = f . p & Ball (p,r) c= ([#] (TOP-REAL n)) \ P ) by A65;
consider p being Point of (TOP-REAL n) such that
A68: ( q = f . p & Ball (p,r) c= ([#] (TOP-REAL n)) \ P ) by A67;
consider x being object such that
A69: ( x in dom f & y = f . x ) by A19;
reconsider p1 = x as Point of (TOP-REAL n) by A69;
reconsider q1 = y as Point of (TOP-REAL (n + 1)) by A69, A36;
q1 in { qy where qy is Point of (TOP-REAL (n + 1)) : |.(qy - q).| < r } by A65, A66, TOPREAL9:def 1;
then consider qy being Point of (TOP-REAL (n + 1)) such that
A70: ( qy = q1 & |.(qy - q).| < r ) ;
f . (p1 - p) = q1 - q by A69, A68, A44;
then |.(p1 - p).| < r by A70, A37;
then p1 in { px where px is Point of (TOP-REAL n) : |.(px - p).| < r } ;
then p1 in Ball (p,r) by TOPREAL9:def 1;
hence y in f .: (([#] (TOP-REAL n)) \ P) by A69, A68, FUNCT_1:def 6; :: thesis:

end;

then A71: f .: (([#] (TOP-REAL n)) \ P) = (union FQ) /\ ([#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))) by SUBSET_1:3;
([#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))) \ (f .: P) = (union FQ) /\ ([#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))) by A71, A35, A56, FUNCT_1:64;
then ([#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))) \ (f .: P) in the topology of (TPlane (p0,(0. (TOP-REAL (n + 1))))) by A61, PRE_TOPC:def 4;
hence f .: P is closed by PRE_TOPC:def 2, PRE_TOPC:def 3; :: thesis:

end;

assume f .: P is closed ; :: thesis:
then ([#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))) \ (f .: P) in the topology of (TPlane (p0,(0. (TOP-REAL (n + 1))))) by PRE_TOPC:def 3, PRE_TOPC:def 2;
then consider Q being Subset of (TOP-REAL (n + 1)) such that
A72: ( Q in the topology of (TOP-REAL (n + 1)) & ([#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))) \ (f .: P) = Q /\ ([#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))) ) by PRE_TOPC:def 4;
for p being Point of (TOP-REAL n) st p in ([#] (TOP-REAL n)) \ P holds
ex r being Real st
( r > 0 & Ball (p,r) c= ([#] (TOP-REAL n)) \ P )

proof

let p be Point of (TOP-REAL n); :: thesis:
assume p in ([#] (TOP-REAL n)) \ P ; :: thesis:
then f . p in f .: (([#] (TOP-REAL n)) \ P) by A18, FUNCT_1:def 6;
then A73: f . p in ([#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))) \ (f .: P) by A56, A35, FUNCT_1:64;
reconsider q = f . p as Point of (TOP-REAL (n + 1)) by A36;
q in Q by A72, A73, XBOOLE_0:def 4;
then consider r being Real such that
A74: ( r > 0 & Ball (q,r) c= Q ) by A72, Th24;
take r ; :: thesis:
thus r > 0 by A74; :: thesis:
let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in Ball (p,r) ; :: thesis:
then x in { px where px is Point of (TOP-REAL n) : |.(px - p).| < r } by TOPREAL9:def 1;
then consider p1 being Point of (TOP-REAL n) such that
A75: ( x = p1 & |.(p1 - p).| < r ) ;
reconsider q1 = f . p1 as Point of (TOP-REAL (n + 1)) by A36;
f . (p1 - p) = q1 - q by A44;
then |.(q1 - q).| < r by A75, A37;
then q1 in { qx where qx is Point of (TOP-REAL (n + 1)) : |.(qx - q).| < r } ;
then q1 in Ball (q,r) by TOPREAL9:def 1;
then q1 in Q /\ ([#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))) by A74, XBOOLE_0:def 4;
then not q1 in f .: P by A72, XBOOLE_0:def 5;
then not x in P by A18, A75, FUNCT_1:def 6;
hence x in ([#] (TOP-REAL n)) \ P by A75, XBOOLE_0:def 5; :: thesis:

end;

then ([#] (TOP-REAL n)) \ P is open by Th24, PRE_TOPC:def 2;
hence P is closed by PRE_TOPC:def 3; :: thesis:

end;

hence TOP-REAL n, TPlane (p0,(0. (TOP-REAL (n + 1)))) are_homeomorphic by T_0TOPSP:def 1, A18, A32, A35, TOPS_2:58; :: thesis: