let n be Nat; :: thesis: for p0 being Point of (TOP-REAL (n + 1)) st p0 = Base_FinSeq ((n + 1),(n + 1)) holds
TOP-REAL n, TPlane (p0,(0. (TOP-REAL (n + 1)))) are_homeomorphic

let p0 be Point of (TOP-REAL (n + 1)); :: thesis: ( p0 = Base_FinSeq ((n + 1),(n + 1)) implies TOP-REAL n, TPlane (p0,(0. (TOP-REAL (n + 1)))) are_homeomorphic )
assume A1: p0 = Base_FinSeq ((n + 1),(n + 1)) ; :: thesis: TOP-REAL n, TPlane (p0,(0. (TOP-REAL (n + 1)))) are_homeomorphic
set T = TOP-REAL n;
set S = TPlane (p0,(0. (TOP-REAL (n + 1))));
defpred S1[ set , set ] means for p being Element of () st \$1 = p holds
\$2 = p ^ ;
A2: for p being Element of () holds p ^ is Element of (TPlane (p0,(0. (TOP-REAL (n + 1)))))
proof
let p be Element of (); :: thesis: p ^ is Element of (TPlane (p0,(0. (TOP-REAL (n + 1)))))
A3: len p = n by CARD_1:def 7;
A4: len () = n + 1 by CARD_1:def 7;
rng () c= REAL ;
then p ^ in REAL (n + 1) by ;
then reconsider q = p ^ 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: ( y in rng (mlt (p0,q)) iff y = r0 )
set f = mlt (p0,q);
A6: now :: thesis: for x being set st x in Seg (n + 1) holds
(mlt (p0,q)) . x = r0
let x be set ; :: thesis: ( x in Seg (n + 1) implies (mlt (p0,q)) . b1 = r0 )
assume x in Seg (n + 1) ; :: thesis: (mlt (p0,q)) . b1 = r0
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 ( k = n + 1 or k <> n + 1 ) ;
suppose A9: k = n + 1 ; :: thesis: (mlt (p0,q)) . b1 = r0
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: verum
end;
suppose k <> n + 1 ; :: thesis: (mlt (p0,q)) . b1 = r0
then p0 . x = 0 by ;
hence (mlt (p0,q)) . x = r0 by A8; :: thesis: verum
end;
end;
end;
hereby :: thesis: ( y = r0 implies y in rng (mlt (p0,q)) )
assume y in rng (mlt (p0,q)) ; :: thesis: y = r0
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: verum
end;
assume A11: y = r0 ; :: thesis: y in rng (mlt (p0,q))
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 ; :: thesis: verum
end;
then mlt (p0,q) = (Seg (n + 1)) --> r0 by ;
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
.= 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 ^ in Plane (p0,(0. (TOP-REAL (n + 1)))) ;
then p ^ in [#] (TPlane (p0,(0. (TOP-REAL (n + 1))))) by PRE_TOPC:def 5;
hence p ^ is Element of (TPlane (p0,(0. (TOP-REAL (n + 1))))) ; :: thesis: verum
end;
A16: for x being Element of () ex y being Element of (TPlane (p0,(0. (TOP-REAL (n + 1))))) st S1[x,y]
proof
let x be Element of (); :: thesis: ex y being Element of (TPlane (p0,(0. (TOP-REAL (n + 1))))) st S1[x,y]
set y = x ^ ;
reconsider y = x ^ as Element of (TPlane (p0,(0. (TOP-REAL (n + 1))))) by A2;
take y ; :: thesis: S1[x,y]
thus S1[x,y] ; :: thesis: verum
end;
consider f being Function of (),(TPlane (p0,(0. (TOP-REAL (n + 1))))) such that
A17: for x being Element of () holds S1[x,f . x] from A18: dom f = [#] () 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: ( y in [#] (TPlane (p0,(0. (TOP-REAL (n + 1))))) iff ex x being object st
( x in dom f & y = f . x ) )

hereby :: thesis: ( ex x being object st
( x in dom f & y = f . x ) implies y in [#] (TPlane (p0,(0. (TOP-REAL (n + 1))))) )
assume y in [#] (TPlane (p0,(0. (TOP-REAL (n + 1))))) ; :: thesis: ex x being object st
( x in dom f & y = f . x )

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: ( x in dom f & y = f . x )
0 + n <= 1 + n by XREAL_1:6;
then A22: len (q1 | n) = n by ;
A23: rng (q1 | n) c= REAL ;
A24: q1 | n in REAL n by ;
hence x in dom f by ; :: thesis: y = f . x
reconsider x1 = x as Element of () by ;
S1[x1,f . x1] by A17;
then A25: f . x = (q1 | n) ^ ;
A26: q = (q1 | n) ^ <*(q . (n + 1))*> by ;
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. () 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 ;
then reconsider p1 = q1 | n as Point of () 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. () in the carrier of () ;
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 ;
len f1 = 1 by FINSEQ_1:39
.= len f3 by FINSEQ_1:39 ;
then |((0. ()),p1)| + |(f1,f3)| = 0 by ;
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 ; :: thesis: verum
end;
given x being object such that A31: ( x in dom f & y = f . x ) ; :: thesis: y in [#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))
reconsider p = x as Element of () by A31;
S1[p,f . p] by A17;
hence y in [#] (TPlane (p0,(0. (TOP-REAL (n + 1))))) by A31; :: thesis: verum
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: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume A33: ( x1 in dom f & x2 in dom f ) ; :: thesis: ( not f . x1 = f . x2 or x1 = x2 )
assume A34: f . x1 = f . x2 ; :: thesis: x1 = x2
reconsider p1 = x1, p2 = x2 as Element of () by A33;
( f . p1 = p1 ^ & f . p2 = p2 ^ ) by A17;
hence x1 = x2 by ; :: thesis: verum
end;
then A35: f is one-to-one ;
set T1 = TOP-REAL (n + 1);
A36: for p1 being Point of () holds f . p1 is Point of (TOP-REAL (n + 1))
proof
let p1 be Point of (); :: thesis: f . p1 is Point of (TOP-REAL (n + 1))
[#] (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: verum
end;
A37: for p1 being Point of ()
for q1 being Point of (TOP-REAL (n + 1)) st q1 = f . p1 holds
|.p1.| = |.q1.|
proof
let p1 be Point of (); :: thesis: for q1 being Point of (TOP-REAL (n + 1)) st q1 = f . p1 holds
|.p1.| = |.q1.|

let q1 be Point of (TOP-REAL (n + 1)); :: thesis: ( q1 = f . p1 implies |.p1.| = |.q1.| )
assume q1 = f . p1 ; :: thesis: |.p1.| = |.q1.|
then A38: q1 = p1 ^ 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 ^ ) | (dom p1) by
.= p1 by FINSEQ_1:21 ;
A41: x . (n + 1) = 0 by ;
A42: |.q1.| ^2 = (|.p1.| ^2) + () by
.= (|.p1.| ^2) + () 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
.= |.q1.| by ;
:: thesis: verum
end;
A44: for p1, p2 being Point of ()
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 (); :: thesis: for q1, q2 being Point of (TOP-REAL (n + 1)) st q1 = f . p1 & q2 = f . p2 holds
f . (p1 - p2) = q1 - q2

let q1, q2 be Point of (TOP-REAL (n + 1)); :: thesis: ( q1 = f . p1 & q2 = f . p2 implies f . (p1 - p2) = q1 - q2 )
assume q1 = f . p1 ; :: thesis: ( not q2 = f . p2 or f . (p1 - p2) = q1 - q2 )
then A45: q1 = p1 ^ by A17;
assume q2 = f . p2 ; :: thesis: f . (p1 - p2) = q1 - q2
then A46: q2 = p2 ^ by A17;
A47: f . (p1 - p2) = (p1 - p2) ^ by A17;
reconsider qa = f . (p1 - p2) as Point of (TOP-REAL (n + 1)) by A36;
A48: dom ((p1 - p2) ^ ) = 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) ^ ) . k
proof
let k be Nat; :: thesis: ( k in dom (q1 - q2) implies (q1 - q2) . k = ((p1 - p2) ^ ) . k )
assume k in dom (q1 - q2) ; :: thesis: (q1 - q2) . k = ((p1 - p2) ^ ) . k
then A49: k in Seg (n + 1) by FINSEQ_1:89;
A50: (q1 - q2) . k = (q1 . k) + ((- q2) . k) by
.= (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 ;
per cases ( k in Seg n or k in {(n + 1)} ) by ;
suppose A52: k in Seg n ; :: thesis: (q1 - q2) . k = ((p1 - p2) ^ ) . k
then ( k in dom p1 & k in dom p2 ) by FINSEQ_1:89;
then A53: ( q1 . k = p1 . k & q2 . k = p2 . k ) by ;
k in dom (p1 - p2) by ;
then ((p1 - p2) ^ ) . k = (p1 - p2) . k by FINSEQ_1:def 7
.= (p1 . k) + ((- p2) . k) by
.= (p1 . k) + (((- 1) * p2) . k) by RLVECT_1:16
.= (p1 . k) + ((- 1) * (p2 . k)) by VALUED_1:6 ;
hence (q1 - q2) . k = ((p1 - p2) ^ ) . k by ; :: thesis: verum
end;
suppose k in {(n + 1)} ; :: thesis: (q1 - q2) . k = ((p1 - p2) ^ ) . k
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 ;
len (p1 - p2) = n by CARD_1:def 7;
hence (q1 - q2) . k = ((p1 - p2) ^ ) . k by ; :: thesis: verum
end;
end;
end;
hence f . (p1 - p2) = q1 - q2 by ; :: thesis: verum
end;
A56: f .: ([#] ()) = [#] (TPlane (p0,(0. (TOP-REAL (n + 1))))) by ;
for P being Subset of () holds
( P is closed iff f .: P is closed )
proof
let P be Subset of (); :: thesis: ( P is closed iff f .: P is closed )
hereby :: thesis: ( f .: P is closed implies P is closed )
assume P is closed ; :: thesis: f .: P is closed
then A57: ([#] ()) \ P in the topology of () by ;
set FQ = { (Ball (q,r)) where q is Point of (TOP-REAL (n + 1)), r is Real : ex p being Point of () st
( q = f . p & Ball (p,r) c= ([#] ()) \ 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 () st
( q = f . p & Ball (p,r) c= ([#] ()) \ P )
}
holds
x in bool ([#] (TOP-REAL (n + 1)))
proof
let x be object ; :: thesis: ( x in { (Ball (q,r)) where q is Point of (TOP-REAL (n + 1)), r is Real : ex p being Point of () st
( q = f . p & Ball (p,r) c= ([#] ()) \ P )
}
implies x in bool ([#] (TOP-REAL (n + 1))) )

assume x in { (Ball (q,r)) where q is Point of (TOP-REAL (n + 1)), r is Real : ex p being Point of () st
( q = f . p & Ball (p,r) c= ([#] ()) \ P )
}
; :: thesis: x in bool ([#] (TOP-REAL (n + 1)))
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 () st
( q = f . p & Ball (p,r) c= ([#] ()) \ P ) ) ;
thus x in bool ([#] (TOP-REAL (n + 1))) by A58; :: thesis: verum
end;
then reconsider FQ = { (Ball (q,r)) where q is Point of (TOP-REAL (n + 1)), r is Real : ex p being Point of () st
( q = f . p & Ball (p,r) c= ([#] ()) \ 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: ( Q in FQ implies Q is open )
assume Q in FQ ; :: thesis: Q is open
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 () st
( q = f . p & Ball (p,r) c= ([#] ()) \ P ) ) ;
thus Q is open by A59; :: thesis: verum
end;
set Q = union FQ;
union FQ is open by ;
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 .: (([#] ()) \ 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: ( y in f .: (([#] ()) \ P) iff y in (union FQ) /\ ([#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))) )
hereby :: thesis: ( y in (union FQ) /\ ([#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))) implies y in f .: (([#] ()) \ P) )
assume y in f .: (([#] ()) \ P) ; :: thesis: y in (union FQ) /\ ([#] (TPlane (p0,(0. (TOP-REAL (n + 1))))))
then consider x being object such that
A62: ( x in dom f & x in ([#] ()) \ P & y = f . x ) by FUNCT_1:def 6;
reconsider p = x as Point of () by A62;
reconsider q = y as Point of (TOP-REAL (n + 1)) by ;
consider r being Real such that
A63: ( r > 0 & Ball (p,r) c= ([#] ()) \ P ) by ;
A64: Ball (q,r) in FQ by ;
q in Ball (q,r) by ;
then y in union FQ by ;
hence y in (union FQ) /\ ([#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))) by XBOOLE_0:def 4; :: thesis: verum
end;
assume y in (union FQ) /\ ([#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))) ; :: thesis: y in f .: (([#] ()) \ P)
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 () st
( q = f . p & Ball (p,r) c= ([#] ()) \ P ) by A65;
consider p being Point of () such that
A68: ( q = f . p & Ball (p,r) c= ([#] ()) \ 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 () by A69;
reconsider q1 = y as Point of (TOP-REAL (n + 1)) by ;
q1 in { qy where qy is Point of (TOP-REAL (n + 1)) : |.(qy - q).| < r } by ;
then consider qy being Point of (TOP-REAL (n + 1)) such that
A70: ( qy = q1 & |.(qy - q).| < r ) ;
f . (p1 - p) = q1 - q by ;
then |.(p1 - p).| < r by ;
then p1 in { px where px is Point of () : |.(px - p).| < r } ;
then p1 in Ball (p,r) by TOPREAL9:def 1;
hence y in f .: (([#] ()) \ P) by ; :: thesis: verum
end;
then A71: f .: (([#] ()) \ 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 ;
then ([#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))) \ (f .: P) in the topology of (TPlane (p0,(0. (TOP-REAL (n + 1))))) by ;
hence f .: P is closed by ; :: thesis: verum
end;
assume f .: P is closed ; :: thesis: P is closed
then ([#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))) \ (f .: P) in the topology of (TPlane (p0,(0. (TOP-REAL (n + 1))))) by ;
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 () st p in ([#] ()) \ P holds
ex r being Real st
( r > 0 & Ball (p,r) c= ([#] ()) \ P )
proof
let p be Point of (); :: thesis: ( p in ([#] ()) \ P implies ex r being Real st
( r > 0 & Ball (p,r) c= ([#] ()) \ P ) )

assume p in ([#] ()) \ P ; :: thesis: ex r being Real st
( r > 0 & Ball (p,r) c= ([#] ()) \ P )

then f . p in f .: (([#] ()) \ P) by ;
then A73: f . p in ([#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))) \ (f .: P) by ;
reconsider q = f . p as Point of (TOP-REAL (n + 1)) by A36;
q in Q by ;
then consider r being Real such that
A74: ( r > 0 & Ball (q,r) c= Q ) by ;
take r ; :: thesis: ( r > 0 & Ball (p,r) c= ([#] ()) \ P )
thus r > 0 by A74; :: thesis: Ball (p,r) c= ([#] ()) \ P
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Ball (p,r) or x in ([#] ()) \ P )
assume x in Ball (p,r) ; :: thesis: x in ([#] ()) \ P
then x in { px where px is Point of () : |.(px - p).| < r } by TOPREAL9:def 1;
then consider p1 being Point of () 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 ;
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 ;
then not q1 in f .: P by ;
then not x in P by ;
hence x in ([#] ()) \ P by ; :: thesis: verum
end;
then ([#] ()) \ P is open by ;
hence P is closed by PRE_TOPC:def 3; :: thesis: verum
end;
hence TOP-REAL n, TPlane (p0,(0. (TOP-REAL (n + 1)))) are_homeomorphic by ; :: thesis: verum