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 S_{1}[ 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)))))_{1}[x,y]

A17: for x being Element of (TOP-REAL n) holds S_{1}[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 ) )

for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds

x1 = x2

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))

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

|.p1.| = |.q1.|

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

f . (p1 - p2) = q1 - q2

for P being Subset of (TOP-REAL n) holds

( P is closed iff f .: P is closed )

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 S

$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

A16:
for x being Element of (TOP-REAL n) ex y being Element of (TPlane (p0,(0. (TOP-REAL (n + 1))))) st S
let p be Element of (TOP-REAL n); :: thesis: p ^ <*0*> is Element of (TPlane (p0,(0. (TOP-REAL (n + 1)))))

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 )

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: verum

end;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

then
mlt (p0,q) = (Seg (n + 1)) --> r0
by A5, FUNCOP_1:9, TARSKI:def 1;
let y be object ; :: thesis: ( y in rng (mlt (p0,q)) iff y = r0 )

set f = 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 A12, A5, FUNCT_1:def 3; :: thesis: verum

end;set f = mlt (p0,q);

A6: now :: thesis: for x being set st x in Seg (n + 1) holds

(mlt (p0,q)) . x = r0

(mlt (p0,q)) . x = r0

let x be set ; :: thesis: ( x in Seg (n + 1) implies (mlt (p0,q)) . b_{1} = r0 )

assume x in Seg (n + 1) ; :: thesis: (mlt (p0,q)) . b_{1} = 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;

end;assume x in Seg (n + 1) ; :: thesis: (mlt (p0,q)) . b

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;

hereby :: thesis: ( y = r0 implies y in rng (mlt (p0,q)) )

assume A11:
y = r0
; :: thesis: 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;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

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: verum

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: verum

proof

consider f being Function of (TOP-REAL n),(TPlane (p0,(0. (TOP-REAL (n + 1))))) such that
let x be Element of (TOP-REAL n); :: thesis: ex y being Element of (TPlane (p0,(0. (TOP-REAL (n + 1))))) st S_{1}[x,y]

set y = x ^ <*0*>;

reconsider y = x ^ <*0*> as Element of (TPlane (p0,(0. (TOP-REAL (n + 1))))) by A2;

take y ; :: thesis: S_{1}[x,y]

thus S_{1}[x,y]
; :: thesis: verum

end;set y = x ^ <*0*>;

reconsider y = x ^ <*0*> as Element of (TPlane (p0,(0. (TOP-REAL (n + 1))))) by A2;

take y ; :: thesis: S

thus S

A17: for x being Element of (TOP-REAL n) holds S

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

then A32:
rng f = [#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))
by FUNCT_1:def 3;
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 ) )

reconsider p = x as Element of (TOP-REAL n) by A31;

S_{1}[p,f . p]
by A17;

hence y in [#] (TPlane (p0,(0. (TOP-REAL (n + 1))))) by A31; :: thesis: verum

end;( 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))))) )

given x being object such that A31:
( x in dom f & y = f . x )
; :: thesis: y in [#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))( 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 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: y = f . x

reconsider x1 = x as Element of (TOP-REAL n) by A24, EUCLID:22;

S_{1}[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: verum

end;( 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 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: y = f . x

reconsider x1 = x as Element of (TOP-REAL n) by A24, EUCLID:22;

S

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: verum

reconsider p = x as Element of (TOP-REAL n) by A31;

S

hence y in [#] (TPlane (p0,(0. (TOP-REAL (n + 1))))) by A31; :: thesis: verum

for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds

x1 = x2

proof

then A35:
f is one-to-one
;
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 (TOP-REAL n) by A33;

( f . p1 = p1 ^ <*0*> & f . p2 = p2 ^ <*0*> ) by A17;

hence x1 = x2 by A34, FINSEQ_1:33; :: thesis: verum

end;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 (TOP-REAL n) by A33;

( f . p1 = p1 ^ <*0*> & f . p2 = p2 ^ <*0*> ) by A17;

hence x1 = x2 by A34, FINSEQ_1:33; :: thesis: verum

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

A37:
for p1 being Point of (TOP-REAL n)
let p1 be Point of (TOP-REAL n); :: 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;[#] (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

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

|.p1.| = |.q1.|

proof

A44:
for p1, p2 being Point of (TOP-REAL n)
let p1 be Point of (TOP-REAL n); :: 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 ^ <*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: verum

end;|.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 ^ <*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: verum

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

f . (p1 - p2) = q1 - q2

proof

A56:
f .: ([#] (TOP-REAL n)) = [#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))
by A32, RELSET_1:22;
let p1, p2 be Point of (TOP-REAL n); :: 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 ^ <*0*> by A17;

assume q2 = f . p2 ; :: thesis: f . (p1 - p2) = q1 - q2

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

end;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 ^ <*0*> by A17;

assume q2 = f . p2 ; :: thesis: f . (p1 - p2) = q1 - q2

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

hence
f . (p1 - p2) = q1 - q2
by A47, A48, FINSEQ_1:13; :: thesis: verum
let k be Nat; :: thesis: ( k in dom (q1 - q2) implies (q1 - q2) . k = ((p1 - p2) ^ <*0*>) . k )

assume k in dom (q1 - q2) ; :: thesis: (q1 - q2) . k = ((p1 - p2) ^ <*0*>) . k

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;

end;assume k in dom (q1 - q2) ; :: thesis: (q1 - q2) . k = ((p1 - p2) ^ <*0*>) . k

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
( k in Seg n or k in {(n + 1)} )
by A51, XBOOLE_0:def 3;

end;

suppose A52:
k in Seg n
; :: thesis: (q1 - q2) . k = ((p1 - p2) ^ <*0*>) . 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 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: verum

end;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: verum

suppose
k in {(n + 1)}
; :: thesis: (q1 - q2) . k = ((p1 - p2) ^ <*0*>) . 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 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: verum

end;( 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: verum

for P being Subset of (TOP-REAL n) holds

( P is closed iff f .: P is closed )

proof

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: verum
let P be Subset of (TOP-REAL n); :: thesis: ( P is closed iff f .: 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 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 )

hence P is closed by PRE_TOPC:def 3; :: thesis: verum

end;hereby :: thesis: ( f .: P is closed implies P is closed )

assume
f .: P is closed
; :: thesis: P is closed assume
P is closed
; :: thesis: f .: P is closed

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)))

( 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

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)))))) )

([#] (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: verum

end;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

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
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 (TOP-REAL n) st

( q = f . p & Ball (p,r) c= ([#] (TOP-REAL n)) \ 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 (TOP-REAL n) st

( q = f . p & Ball (p,r) c= ([#] (TOP-REAL n)) \ 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 (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: verum

end;( q = f . p & Ball (p,r) c= ([#] (TOP-REAL n)) \ 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 (TOP-REAL n) st

( q = f . p & Ball (p,r) c= ([#] (TOP-REAL n)) \ 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 (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: verum

( 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

set Q = union FQ;
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 (TOP-REAL n) st

( q = f . p & Ball (p,r) c= ([#] (TOP-REAL n)) \ P ) ) ;

thus Q is open by A59; :: thesis: verum

end;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 (TOP-REAL n) st

( q = f . p & Ball (p,r) c= ([#] (TOP-REAL n)) \ P ) ) ;

thus Q is open by A59; :: thesis: verum

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

then A71:
f .: (([#] (TOP-REAL n)) \ P) = (union FQ) /\ ([#] (TPlane (p0,(0. (TOP-REAL (n + 1))))))
by SUBSET_1:3;
let y be Element of (TPlane (p0,(0. (TOP-REAL (n + 1))))); :: thesis: ( y in f .: (([#] (TOP-REAL n)) \ P) iff y in (union FQ) /\ ([#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))) )

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: verum

end;hereby :: thesis: ( y in (union FQ) /\ ([#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))) implies y in f .: (([#] (TOP-REAL n)) \ P) )

assume
y in (union FQ) /\ ([#] (TPlane (p0,(0. (TOP-REAL (n + 1))))))
; :: thesis: y in f .: (([#] (TOP-REAL n)) \ P)assume
y in f .: (([#] (TOP-REAL n)) \ 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 ([#] (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: verum

end;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: verum

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: verum

([#] (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: verum

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

then
([#] (TOP-REAL n)) \ P is open
by Th24, PRE_TOPC:def 2;
let p be Point of (TOP-REAL n); :: thesis: ( p in ([#] (TOP-REAL n)) \ P implies ex r being Real st

( r > 0 & Ball (p,r) c= ([#] (TOP-REAL n)) \ P ) )

assume p in ([#] (TOP-REAL n)) \ P ; :: thesis: ex r being Real st

( r > 0 & Ball (p,r) c= ([#] (TOP-REAL n)) \ P )

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: ( r > 0 & Ball (p,r) c= ([#] (TOP-REAL n)) \ P )

thus r > 0 by A74; :: thesis: Ball (p,r) c= ([#] (TOP-REAL n)) \ P

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Ball (p,r) or x in ([#] (TOP-REAL n)) \ P )

assume x in Ball (p,r) ; :: thesis: x in ([#] (TOP-REAL n)) \ P

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: verum

end;( r > 0 & Ball (p,r) c= ([#] (TOP-REAL n)) \ P ) )

assume p in ([#] (TOP-REAL n)) \ P ; :: thesis: ex r being Real st

( r > 0 & Ball (p,r) c= ([#] (TOP-REAL n)) \ P )

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: ( r > 0 & Ball (p,r) c= ([#] (TOP-REAL n)) \ P )

thus r > 0 by A74; :: thesis: Ball (p,r) c= ([#] (TOP-REAL n)) \ P

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Ball (p,r) or x in ([#] (TOP-REAL n)) \ P )

assume x in Ball (p,r) ; :: thesis: x in ([#] (TOP-REAL n)) \ P

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: verum

hence P is closed by PRE_TOPC:def 3; :: thesis: verum