let n be Nat; :: thesis: for p being Point of (TOP-REAL n)

for A being Subset of (TOP-REAL n)

for r being Real st not p in A & r > 0 holds

ex h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | (Sphere (p,r))) st

( h is continuous & h | (Sphere (p,r)) = id (A /\ (Sphere (p,r))) )

let p be Point of (TOP-REAL n); :: thesis: for A being Subset of (TOP-REAL n)

for r being Real st not p in A & r > 0 holds

ex h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | (Sphere (p,r))) st

( h is continuous & h | (Sphere (p,r)) = id (A /\ (Sphere (p,r))) )

let A be Subset of (TOP-REAL n); :: thesis: for r being Real st not p in A & r > 0 holds

ex h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | (Sphere (p,r))) st

( h is continuous & h | (Sphere (p,r)) = id (A /\ (Sphere (p,r))) )

let r be Real; :: thesis: ( not p in A & r > 0 implies ex h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | (Sphere (p,r))) st

( h is continuous & h | (Sphere (p,r)) = id (A /\ (Sphere (p,r))) ) )

set TR = TOP-REAL n;

assume that

A1: not p in A and

A2: r > 0 ; :: thesis: ex h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | (Sphere (p,r))) st

( h is continuous & h | (Sphere (p,r)) = id (A /\ (Sphere (p,r))) )

set S = Sphere (p,r);

for A being Subset of (TOP-REAL n)

for r being Real st not p in A & r > 0 holds

ex h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | (Sphere (p,r))) st

( h is continuous & h | (Sphere (p,r)) = id (A /\ (Sphere (p,r))) )

let p be Point of (TOP-REAL n); :: thesis: for A being Subset of (TOP-REAL n)

for r being Real st not p in A & r > 0 holds

ex h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | (Sphere (p,r))) st

( h is continuous & h | (Sphere (p,r)) = id (A /\ (Sphere (p,r))) )

let A be Subset of (TOP-REAL n); :: thesis: for r being Real st not p in A & r > 0 holds

ex h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | (Sphere (p,r))) st

( h is continuous & h | (Sphere (p,r)) = id (A /\ (Sphere (p,r))) )

let r be Real; :: thesis: ( not p in A & r > 0 implies ex h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | (Sphere (p,r))) st

( h is continuous & h | (Sphere (p,r)) = id (A /\ (Sphere (p,r))) ) )

set TR = TOP-REAL n;

assume that

A1: not p in A and

A2: r > 0 ; :: thesis: ex h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | (Sphere (p,r))) st

( h is continuous & h | (Sphere (p,r)) = id (A /\ (Sphere (p,r))) )

set S = Sphere (p,r);

per cases
( A is empty or not A is empty )
;

end;

suppose A3:
A is empty
; :: thesis: ex h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | (Sphere (p,r))) st

( h is continuous & h | (Sphere (p,r)) = id (A /\ (Sphere (p,r))) )

( h is continuous & h | (Sphere (p,r)) = id (A /\ (Sphere (p,r))) )

set h = the continuous Function of ((TOP-REAL n) | A),(TOP-REAL n);

reconsider H = the continuous Function of ((TOP-REAL n) | A),(TOP-REAL n) as Function of ((TOP-REAL n) | A),((TOP-REAL n) | (Sphere (p,r))) by A3;

take H ; :: thesis: ( H is continuous & H | (Sphere (p,r)) = id (A /\ (Sphere (p,r))) )

thus ( H is continuous & H | (Sphere (p,r)) = id (A /\ (Sphere (p,r))) ) by A3, PRE_TOPC:27; :: thesis: verum

end;reconsider H = the continuous Function of ((TOP-REAL n) | A),(TOP-REAL n) as Function of ((TOP-REAL n) | A),((TOP-REAL n) | (Sphere (p,r))) by A3;

take H ; :: thesis: ( H is continuous & H | (Sphere (p,r)) = id (A /\ (Sphere (p,r))) )

thus ( H is continuous & H | (Sphere (p,r)) = id (A /\ (Sphere (p,r))) ) by A3, PRE_TOPC:27; :: thesis: verum

suppose A4:
not A is empty
; :: thesis: ex h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | (Sphere (p,r))) st

( h is continuous & h | (Sphere (p,r)) = id (A /\ (Sphere (p,r))) )

( h is continuous & h | (Sphere (p,r)) = id (A /\ (Sphere (p,r))) )

A <> {p}
by A1, TARSKI:def 1;

then A5: A \ {p} <> {} by A4, ZFMISC_1:58;

set TRS = (TOP-REAL n) | (Sphere (p,r));

set nN = n NormF ;

set t = transl ((- p),(TOP-REAL n));

set P = transl (p,(TOP-REAL n));

A6: A \ {p} c= the carrier of (TOP-REAL n) \ {p} by XBOOLE_1:33;

the carrier of (TOP-REAL n) \ {p} = {p} ` by SUBSET_1:def 4;

then reconsider cTRp = the carrier of (TOP-REAL n) \ {p} as non empty open Subset of (TOP-REAL n) by A5, A6;

set TRp = (TOP-REAL n) | cTRp;

set tt = (transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp);

A7: [#] ((TOP-REAL n) | cTRp) = cTRp by PRE_TOPC:def 5;

then reconsider AA = A as Subset of ((TOP-REAL n) | cTRp) by A1, ZFMISC_1:57, A6;

reconsider Ir = ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp)) [#] r as Function of ((TOP-REAL n) | cTRp),(TOP-REAL n) by TOPREALC:37;

reconsider IrNt = Ir </> ((n NormF) * ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp))) as Function of ((TOP-REAL n) | cTRp),(TOP-REAL n) by TOPREALC:46;

A8: (transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp) = (transl ((- p),(TOP-REAL n))) | the carrier of ((TOP-REAL n) | cTRp) by TMAP_1:def 4;

not 0 in rng ((n NormF) * ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp)))

then reconsider IrNt = IrNt as continuous Function of ((TOP-REAL n) | cTRp),(TOP-REAL n) ;

set h = ((transl (p,(TOP-REAL n))) * IrNt) | (((TOP-REAL n) | cTRp) | AA);

A13: ((transl (p,(TOP-REAL n))) * IrNt) | (((TOP-REAL n) | cTRp) | AA) = ((transl (p,(TOP-REAL n))) * IrNt) | the carrier of (((TOP-REAL n) | cTRp) | AA) by TMAP_1:def 4;

reconsider h = ((transl (p,(TOP-REAL n))) * IrNt) | (((TOP-REAL n) | cTRp) | AA) as continuous Function of (((TOP-REAL n) | cTRp) | AA),(TOP-REAL n) by A4;

((TOP-REAL n) | cTRp) | AA = (TOP-REAL n) | A by PRE_TOPC:7, A7;

then reconsider h = h as continuous Function of ((TOP-REAL n) | A),(TOP-REAL n) ;

A14: [#] ((TOP-REAL n) | A) = A by PRE_TOPC:def 5;

then A15: dom h = A by FUNCT_2:def 1;

A16: dom ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp)) = cTRp by A7, FUNCT_2:def 1;

A17: rng h c= Sphere (p,r)

then reconsider h = h as Function of ((TOP-REAL n) | A),((TOP-REAL n) | (Sphere (p,r))) by A17, A14, A15, FUNCT_2:2;

A29: dom (h | (Sphere (p,r))) = A /\ (Sphere (p,r)) by A15, RELAT_1:61;

A31: for x being object st x in dom (h | (Sphere (p,r))) holds

(h | (Sphere (p,r))) . x = (id (A /\ (Sphere (p,r)))) . x

thus ( h is continuous & h | (Sphere (p,r)) = id (A /\ (Sphere (p,r))) ) by A31, A15, PRE_TOPC:27, RELAT_1:61; :: thesis: verum

end;then A5: A \ {p} <> {} by A4, ZFMISC_1:58;

set TRS = (TOP-REAL n) | (Sphere (p,r));

set nN = n NormF ;

set t = transl ((- p),(TOP-REAL n));

set P = transl (p,(TOP-REAL n));

A6: A \ {p} c= the carrier of (TOP-REAL n) \ {p} by XBOOLE_1:33;

the carrier of (TOP-REAL n) \ {p} = {p} ` by SUBSET_1:def 4;

then reconsider cTRp = the carrier of (TOP-REAL n) \ {p} as non empty open Subset of (TOP-REAL n) by A5, A6;

set TRp = (TOP-REAL n) | cTRp;

set tt = (transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp);

A7: [#] ((TOP-REAL n) | cTRp) = cTRp by PRE_TOPC:def 5;

then reconsider AA = A as Subset of ((TOP-REAL n) | cTRp) by A1, ZFMISC_1:57, A6;

reconsider Ir = ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp)) [#] r as Function of ((TOP-REAL n) | cTRp),(TOP-REAL n) by TOPREALC:37;

reconsider IrNt = Ir </> ((n NormF) * ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp))) as Function of ((TOP-REAL n) | cTRp),(TOP-REAL n) by TOPREALC:46;

A8: (transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp) = (transl ((- p),(TOP-REAL n))) | the carrier of ((TOP-REAL n) | cTRp) by TMAP_1:def 4;

not 0 in rng ((n NormF) * ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp)))

proof

then
(n NormF) * ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp)) is non-empty
by RELAT_1:def 9;
assume
0 in rng ((n NormF) * ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp)))
; :: thesis: contradiction

then consider x being object such that

A9: x in dom ((n NormF) * ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp))) and

A10: ((n NormF) * ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp))) . x = 0 by FUNCT_1:def 3;

((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp)) . x in dom (n NormF) by A9, FUNCT_1:11;

then reconsider Tx = ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp)) . x as Point of (TOP-REAL n) ;

reconsider Tx = Tx as Element of REAL n by EUCLID:22;

A11: x in dom ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp)) by A9, FUNCT_1:11;

then A12: (transl ((- p),(TOP-REAL n))) . x = ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp)) . x by A8, FUNCT_1:47;

x in dom (transl ((- p),(TOP-REAL n))) by A11, A8, RELAT_1:57;

then reconsider X = x as Point of (TOP-REAL n) ;

0 = (n NormF) . Tx by A9, FUNCT_1:12, A10

.= |.Tx.| by JGRAPH_4:def 1 ;

then 0* n = Tx by EUCLID:8;

then 0. (TOP-REAL n) = Tx by EUCLID:70

.= (- p) + X by A12, RLTOPSP1:def 10 ;

then X = - (- p) by RLVECT_1:def 10

.= p ;

then x in {p} by TARSKI:def 1;

hence contradiction by A9, A7, XBOOLE_0:def 5; :: thesis: verum

end;then consider x being object such that

A9: x in dom ((n NormF) * ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp))) and

A10: ((n NormF) * ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp))) . x = 0 by FUNCT_1:def 3;

((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp)) . x in dom (n NormF) by A9, FUNCT_1:11;

then reconsider Tx = ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp)) . x as Point of (TOP-REAL n) ;

reconsider Tx = Tx as Element of REAL n by EUCLID:22;

A11: x in dom ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp)) by A9, FUNCT_1:11;

then A12: (transl ((- p),(TOP-REAL n))) . x = ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp)) . x by A8, FUNCT_1:47;

x in dom (transl ((- p),(TOP-REAL n))) by A11, A8, RELAT_1:57;

then reconsider X = x as Point of (TOP-REAL n) ;

0 = (n NormF) . Tx by A9, FUNCT_1:12, A10

.= |.Tx.| by JGRAPH_4:def 1 ;

then 0* n = Tx by EUCLID:8;

then 0. (TOP-REAL n) = Tx by EUCLID:70

.= (- p) + X by A12, RLTOPSP1:def 10 ;

then X = - (- p) by RLVECT_1:def 10

.= p ;

then x in {p} by TARSKI:def 1;

hence contradiction by A9, A7, XBOOLE_0:def 5; :: thesis: verum

then reconsider IrNt = IrNt as continuous Function of ((TOP-REAL n) | cTRp),(TOP-REAL n) ;

set h = ((transl (p,(TOP-REAL n))) * IrNt) | (((TOP-REAL n) | cTRp) | AA);

A13: ((transl (p,(TOP-REAL n))) * IrNt) | (((TOP-REAL n) | cTRp) | AA) = ((transl (p,(TOP-REAL n))) * IrNt) | the carrier of (((TOP-REAL n) | cTRp) | AA) by TMAP_1:def 4;

reconsider h = ((transl (p,(TOP-REAL n))) * IrNt) | (((TOP-REAL n) | cTRp) | AA) as continuous Function of (((TOP-REAL n) | cTRp) | AA),(TOP-REAL n) by A4;

((TOP-REAL n) | cTRp) | AA = (TOP-REAL n) | A by PRE_TOPC:7, A7;

then reconsider h = h as continuous Function of ((TOP-REAL n) | A),(TOP-REAL n) ;

A14: [#] ((TOP-REAL n) | A) = A by PRE_TOPC:def 5;

then A15: dom h = A by FUNCT_2:def 1;

A16: dom ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp)) = cTRp by A7, FUNCT_2:def 1;

A17: rng h c= Sphere (p,r)

proof

[#] ((TOP-REAL n) | (Sphere (p,r))) = Sphere (p,r)
by PRE_TOPC:def 5;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng h or y in Sphere (p,r) )

assume y in rng h ; :: thesis: y in Sphere (p,r)

then consider x being object such that

A18: x in dom h and

A19: h . x = y by FUNCT_1:def 3;

reconsider x = x as Point of (TOP-REAL n) by A18, A15;

((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp)) . x = (transl ((- p),(TOP-REAL n))) . x by A7, A18, A15, FUNCT_1:47, A8, A16;

then A20: ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp)) . x = (- p) + x by RLTOPSP1:def 10;

dom ((n NormF) * ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp))) = cTRp by A7, FUNCT_2:def 1;

then ((n NormF) * ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp))) . x = (n NormF) . (((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp)) . x) by A7, A18, A15, FUNCT_1:12;

then A21: ((n NormF) * ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp))) . x = |.((- p) + x).| by A20, JGRAPH_4:def 1;

A22: x in dom ((transl (p,(TOP-REAL n))) * IrNt) by A13, A18, RELAT_1:57;

then x in dom IrNt by FUNCT_1:11;

then A23: IrNt . x = (Ir . x) (/) (((n NormF) * ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp))) . x) by VALUED_2:72;

dom Ir = cTRp by A7, FUNCT_2:def 1;

then Ir . x = r * ((- p) + x) by A20, A7, A18, A15, VALUED_2:def 39;

then A24: IrNt . x = (1 / |.((- p) + x).|) * (r * ((- p) + x)) by A21, A23, VALUED_2:def 32;

then reconsider Fx = IrNt . x as Point of (TOP-REAL n) ;

h . x = ((transl (p,(TOP-REAL n))) * IrNt) . x by A13, A18, FUNCT_1:47;

then A25: h . x = (transl (p,(TOP-REAL n))) . Fx by A22, FUNCT_1:12

.= p + Fx by RLTOPSP1:def 10 ;

- (- p) = p ;

then (- p) + x <> 0. (TOP-REAL n) by A18, A1, A15, RLVECT_1:6;

then A26: (- p) + x <> 0* n by EUCLID:70;

A27: (- p) + x is Element of REAL n by EUCLID:22;

A28: (p + Fx) - p = Fx + (p + (- p)) by RLVECT_1:def 3

.= Fx + (0. (TOP-REAL n)) by RLVECT_1:def 10

.= Fx by RLVECT_1:def 4 ;

|.Fx.| = |.(((1 / |.((- p) + x).|) * r) * ((- p) + x)).| by A24, RLVECT_1:def 7

.= |.((1 / |.((- p) + x).|) * r).| * |.((- p) + x).| by EUCLID:11

.= (|.(1 / |.((- p) + x).|).| * |.r.|) * |.((- p) + x).| by COMPLEX1:65

.= (|.(1 / |.((- p) + x).|).| * r) * |.((- p) + x).| by ABSVALUE:def 1, A2

.= (|.(1 / |.((- p) + x).|).| * r) * |.|.((- p) + x).|.| by ABSVALUE:def 1

.= (|.(1 / |.((- p) + x).|).| * |.|.((- p) + x).|.|) * r

.= 1 * r by ABSVALUE:6, A26, EUCLID:8, A27

.= r ;

hence y in Sphere (p,r) by A28, A25, A19; :: thesis: verum

end;assume y in rng h ; :: thesis: y in Sphere (p,r)

then consider x being object such that

A18: x in dom h and

A19: h . x = y by FUNCT_1:def 3;

reconsider x = x as Point of (TOP-REAL n) by A18, A15;

((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp)) . x = (transl ((- p),(TOP-REAL n))) . x by A7, A18, A15, FUNCT_1:47, A8, A16;

then A20: ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp)) . x = (- p) + x by RLTOPSP1:def 10;

dom ((n NormF) * ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp))) = cTRp by A7, FUNCT_2:def 1;

then ((n NormF) * ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp))) . x = (n NormF) . (((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp)) . x) by A7, A18, A15, FUNCT_1:12;

then A21: ((n NormF) * ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp))) . x = |.((- p) + x).| by A20, JGRAPH_4:def 1;

A22: x in dom ((transl (p,(TOP-REAL n))) * IrNt) by A13, A18, RELAT_1:57;

then x in dom IrNt by FUNCT_1:11;

then A23: IrNt . x = (Ir . x) (/) (((n NormF) * ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp))) . x) by VALUED_2:72;

dom Ir = cTRp by A7, FUNCT_2:def 1;

then Ir . x = r * ((- p) + x) by A20, A7, A18, A15, VALUED_2:def 39;

then A24: IrNt . x = (1 / |.((- p) + x).|) * (r * ((- p) + x)) by A21, A23, VALUED_2:def 32;

then reconsider Fx = IrNt . x as Point of (TOP-REAL n) ;

h . x = ((transl (p,(TOP-REAL n))) * IrNt) . x by A13, A18, FUNCT_1:47;

then A25: h . x = (transl (p,(TOP-REAL n))) . Fx by A22, FUNCT_1:12

.= p + Fx by RLTOPSP1:def 10 ;

- (- p) = p ;

then (- p) + x <> 0. (TOP-REAL n) by A18, A1, A15, RLVECT_1:6;

then A26: (- p) + x <> 0* n by EUCLID:70;

A27: (- p) + x is Element of REAL n by EUCLID:22;

A28: (p + Fx) - p = Fx + (p + (- p)) by RLVECT_1:def 3

.= Fx + (0. (TOP-REAL n)) by RLVECT_1:def 10

.= Fx by RLVECT_1:def 4 ;

|.Fx.| = |.(((1 / |.((- p) + x).|) * r) * ((- p) + x)).| by A24, RLVECT_1:def 7

.= |.((1 / |.((- p) + x).|) * r).| * |.((- p) + x).| by EUCLID:11

.= (|.(1 / |.((- p) + x).|).| * |.r.|) * |.((- p) + x).| by COMPLEX1:65

.= (|.(1 / |.((- p) + x).|).| * r) * |.((- p) + x).| by ABSVALUE:def 1, A2

.= (|.(1 / |.((- p) + x).|).| * r) * |.|.((- p) + x).|.| by ABSVALUE:def 1

.= (|.(1 / |.((- p) + x).|).| * |.|.((- p) + x).|.|) * r

.= 1 * r by ABSVALUE:6, A26, EUCLID:8, A27

.= r ;

hence y in Sphere (p,r) by A28, A25, A19; :: thesis: verum

then reconsider h = h as Function of ((TOP-REAL n) | A),((TOP-REAL n) | (Sphere (p,r))) by A17, A14, A15, FUNCT_2:2;

A29: dom (h | (Sphere (p,r))) = A /\ (Sphere (p,r)) by A15, RELAT_1:61;

A31: for x being object st x in dom (h | (Sphere (p,r))) holds

(h | (Sphere (p,r))) . x = (id (A /\ (Sphere (p,r)))) . x

proof

take
h
; :: thesis: ( h is continuous & h | (Sphere (p,r)) = id (A /\ (Sphere (p,r))) )
let y be object ; :: thesis: ( y in dom (h | (Sphere (p,r))) implies (h | (Sphere (p,r))) . y = (id (A /\ (Sphere (p,r)))) . y )

assume A32: y in dom (h | (Sphere (p,r))) ; :: thesis: (h | (Sphere (p,r))) . y = (id (A /\ (Sphere (p,r)))) . y

then reconsider x = y as Point of (TOP-REAL n) by A29;

A33: x in dom h by A32, RELAT_1:57;

then A34: h . x = ((transl (p,(TOP-REAL n))) * IrNt) . x by A13, FUNCT_1:47;

((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp)) . x = (transl ((- p),(TOP-REAL n))) . x by A7, A33, A15, FUNCT_1:47, A8, A16;

then A35: ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp)) . x = (- p) + x by RLTOPSP1:def 10;

x - p = (- p) + x ;

then A36: |.((- p) + x).| = r by A32, TOPREAL9:9;

A37: x in dom ((transl (p,(TOP-REAL n))) * IrNt) by A13, A33, RELAT_1:57;

then x in dom IrNt by FUNCT_1:11;

then A38: IrNt . x = (Ir . x) (/) (((n NormF) * ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp))) . x) by VALUED_2:72;

dom ((n NormF) * ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp))) = cTRp by A7, FUNCT_2:def 1;

then ((n NormF) * ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp))) . x = (n NormF) . (((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp)) . x) by A7, A33, A15, FUNCT_1:12;

then A39: ((n NormF) * ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp))) . x = |.((- p) + x).| by A35, JGRAPH_4:def 1;

dom Ir = cTRp by A7, FUNCT_2:def 1;

then Ir . x = r * ((- p) + x) by A35, A7, A33, A15, VALUED_2:def 39;

then A40: IrNt . x = (1 / |.((- p) + x).|) * (r * ((- p) + x)) by A39, A38, VALUED_2:def 32

.= ((1 / r) * r) * ((- p) + x) by A36, RLVECT_1:def 7

.= 1 * ((- p) + x) by XCMPLX_1:87, A2

.= (- p) + x by RLVECT_1:def 8 ;

thus (h | (Sphere (p,r))) . y = h . x by A32, FUNCT_1:47

.= (transl (p,(TOP-REAL n))) . ((- p) + x) by A34, A37, FUNCT_1:12, A40

.= p + ((- p) + x) by RLTOPSP1:def 10

.= (p + (- p)) + x by RLVECT_1:def 3

.= (0. (TOP-REAL n)) + x by RLVECT_1:def 10

.= x by RLVECT_1:def 4

.= (id (A /\ (Sphere (p,r)))) . y by A32, A29, FUNCT_1:17 ; :: thesis: verum

end;assume A32: y in dom (h | (Sphere (p,r))) ; :: thesis: (h | (Sphere (p,r))) . y = (id (A /\ (Sphere (p,r)))) . y

then reconsider x = y as Point of (TOP-REAL n) by A29;

A33: x in dom h by A32, RELAT_1:57;

then A34: h . x = ((transl (p,(TOP-REAL n))) * IrNt) . x by A13, FUNCT_1:47;

((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp)) . x = (transl ((- p),(TOP-REAL n))) . x by A7, A33, A15, FUNCT_1:47, A8, A16;

then A35: ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp)) . x = (- p) + x by RLTOPSP1:def 10;

x - p = (- p) + x ;

then A36: |.((- p) + x).| = r by A32, TOPREAL9:9;

A37: x in dom ((transl (p,(TOP-REAL n))) * IrNt) by A13, A33, RELAT_1:57;

then x in dom IrNt by FUNCT_1:11;

then A38: IrNt . x = (Ir . x) (/) (((n NormF) * ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp))) . x) by VALUED_2:72;

dom ((n NormF) * ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp))) = cTRp by A7, FUNCT_2:def 1;

then ((n NormF) * ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp))) . x = (n NormF) . (((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp)) . x) by A7, A33, A15, FUNCT_1:12;

then A39: ((n NormF) * ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp))) . x = |.((- p) + x).| by A35, JGRAPH_4:def 1;

dom Ir = cTRp by A7, FUNCT_2:def 1;

then Ir . x = r * ((- p) + x) by A35, A7, A33, A15, VALUED_2:def 39;

then A40: IrNt . x = (1 / |.((- p) + x).|) * (r * ((- p) + x)) by A39, A38, VALUED_2:def 32

.= ((1 / r) * r) * ((- p) + x) by A36, RLVECT_1:def 7

.= 1 * ((- p) + x) by XCMPLX_1:87, A2

.= (- p) + x by RLVECT_1:def 8 ;

thus (h | (Sphere (p,r))) . y = h . x by A32, FUNCT_1:47

.= (transl (p,(TOP-REAL n))) . ((- p) + x) by A34, A37, FUNCT_1:12, A40

.= p + ((- p) + x) by RLTOPSP1:def 10

.= (p + (- p)) + x by RLVECT_1:def 3

.= (0. (TOP-REAL n)) + x by RLVECT_1:def 10

.= x by RLVECT_1:def 4

.= (id (A /\ (Sphere (p,r)))) . y by A32, A29, FUNCT_1:17 ; :: thesis: verum

thus ( h is continuous & h | (Sphere (p,r)) = id (A /\ (Sphere (p,r))) ) by A31, A15, PRE_TOPC:27, RELAT_1:61; :: thesis: verum