let sn be Real; ( - 1 < sn & sn < 1 implies ( sn -FanMorphW is Function of (TOP-REAL 2),(TOP-REAL 2) & rng (sn -FanMorphW ) = the carrier of (TOP-REAL 2) ) )
assume that
A1:
- 1 < sn
and
A2:
sn < 1
; ( sn -FanMorphW is Function of (TOP-REAL 2),(TOP-REAL 2) & rng (sn -FanMorphW ) = the carrier of (TOP-REAL 2) )
thus
sn -FanMorphW is Function of (TOP-REAL 2),(TOP-REAL 2)
; rng (sn -FanMorphW ) = the carrier of (TOP-REAL 2)
for f being Function of (TOP-REAL 2),(TOP-REAL 2) st f = sn -FanMorphW holds
rng (sn -FanMorphW ) = the carrier of (TOP-REAL 2)
proof
let f be
Function of
(TOP-REAL 2),
(TOP-REAL 2);
( f = sn -FanMorphW implies rng (sn -FanMorphW ) = the carrier of (TOP-REAL 2) )
assume A3:
f = sn -FanMorphW
;
rng (sn -FanMorphW ) = the carrier of (TOP-REAL 2)
A4:
dom f = the
carrier of
(TOP-REAL 2)
by FUNCT_2:def 1;
the
carrier of
(TOP-REAL 2) c= rng f
proof
let y be
set ;
TARSKI:def 3 ( not y in the carrier of (TOP-REAL 2) or y in rng f )
assume
y in the
carrier of
(TOP-REAL 2)
;
y in rng f
then reconsider p2 =
y as
Point of
(TOP-REAL 2) ;
set q =
p2;
now per cases
( p2 `1 >= 0 or ( (p2 `2 ) / |.p2.| >= 0 & p2 `1 <= 0 & p2 <> 0. (TOP-REAL 2) ) or ( (p2 `2 ) / |.p2.| < 0 & p2 `1 <= 0 & p2 <> 0. (TOP-REAL 2) ) )
by JGRAPH_2:11;
case A5:
(
(p2 `2 ) / |.p2.| >= 0 &
p2 `1 <= 0 &
p2 <> 0. (TOP-REAL 2) )
;
ex x being set st
( x in dom (sn -FanMorphW ) & y = (sn -FanMorphW ) . x )A6:
- (- (1 + sn)) > 0
by A1, XREAL_1:150;
A7:
1
- sn >= 0
by A2, XREAL_1:151;
then
((p2 `2 ) / |.p2.|) * (1 - sn) >= 0
by A5;
then
- (1 + sn) <= ((p2 `2 ) / |.p2.|) * (1 - sn)
by A6;
then A8:
((- 1) - sn) + sn <= (((p2 `2 ) / |.p2.|) * (1 - sn)) + sn
by XREAL_1:9;
set px =
|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn))]|;
A9:
|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn))]| `2 = |.p2.| * ((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn)
by EUCLID:56;
|.p2.| <> 0
by A5, TOPRNS_1:25;
then A10:
|.p2.| ^2 > 0
by SQUARE_1:74;
A11:
|.p2.| > 0
by A5, Lm1;
A12:
dom (sn -FanMorphW ) = the
carrier of
(TOP-REAL 2)
by FUNCT_2:def 1;
A13:
1
- sn > 0
by A2, XREAL_1:151;
0 <= (p2 `1 ) ^2
by XREAL_1:65;
then
(
|.p2.| ^2 = ((p2 `1 ) ^2 ) + ((p2 `2 ) ^2 ) &
0 + ((p2 `2 ) ^2 ) <= ((p2 `1 ) ^2 ) + ((p2 `2 ) ^2 ) )
by JGRAPH_3:10, XREAL_1:9;
then
((p2 `2 ) ^2 ) / (|.p2.| ^2 ) <= (|.p2.| ^2 ) / (|.p2.| ^2 )
by XREAL_1:74;
then
((p2 `2 ) ^2 ) / (|.p2.| ^2 ) <= 1
by A10, XCMPLX_1:60;
then
((p2 `2 ) / |.p2.|) ^2 <= 1
by XCMPLX_1:77;
then
(p2 `2 ) / |.p2.| <= 1
by SQUARE_1:121;
then
((p2 `2 ) / |.p2.|) * (1 - sn) <= 1
* (1 - sn)
by A13, XREAL_1:66;
then
((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn) - sn <= 1
- sn
;
then
(((p2 `2 ) / |.p2.|) * (1 - sn)) + sn <= 1
by XREAL_1:11;
then
1
^2 >= ((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn) ^2
by A8, SQUARE_1:119;
then A14:
1
- (((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn) ^2 ) >= 0
by XREAL_1:50;
then A15:
sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn) ^2 )) >= 0
by SQUARE_1:def 4;
A16:
|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn))]| `1 = - (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn) ^2 ))))
by EUCLID:56;
then |.|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn))]|.| ^2 =
((- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn) ^2 ))))) ^2 ) + ((|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn)) ^2 )
by A9, JGRAPH_3:10
.=
((|.p2.| ^2 ) * ((sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn) ^2 ))) ^2 )) + ((|.p2.| ^2 ) * (((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn) ^2 ))
;
then A17:
|.|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn))]|.| ^2 =
((|.p2.| ^2 ) * (1 - (((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn) ^2 ))) + ((|.p2.| ^2 ) * (((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn) ^2 ))
by A14, SQUARE_1:def 4
.=
|.p2.| ^2
;
then A18:
|.|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn))]|.| =
sqrt (|.p2.| ^2 )
by SQUARE_1:89
.=
|.p2.|
by SQUARE_1:89
;
then A19:
|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn))]| <> 0. (TOP-REAL 2)
by A5, TOPRNS_1:24, TOPRNS_1:25;
(((p2 `2 ) / |.p2.|) * (1 - sn)) + sn >= 0 + sn
by A5, A7, XREAL_1:9;
then
(|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn))]| `2 ) / |.|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn))]|.| >= sn
by A5, A9, A18, TOPRNS_1:25, XCMPLX_1:90;
then A20:
(sn -FanMorphW ) . |[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn))]| = |[(|.|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn))]|.| * (- (sqrt (1 - (((((|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn))]| `2 ) / |.|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn))]|.|) - sn) / (1 - sn)) ^2 ))))),(|.|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn))]|.| * ((((|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn))]| `2 ) / |.|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn))]|.|) - sn) / (1 - sn)))]|
by A1, A2, A16, A15, A19, Th25;
A21:
|.|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn))]|.| * (- (sqrt (((p2 `1 ) / |.p2.|) ^2 ))) =
|.|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn))]|.| * (- (- ((p2 `1 ) / |.p2.|)))
by A5, SQUARE_1:90
.=
p2 `1
by A11, A18, XCMPLX_1:88
;
A22:
|.|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn))]|.| * ((((|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn))]| `2 ) / |.|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn))]|.|) - sn) / (1 - sn)) =
|.p2.| * ((((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn) - sn) / (1 - sn))
by A5, A9, A18, TOPRNS_1:25, XCMPLX_1:90
.=
|.p2.| * ((p2 `2 ) / |.p2.|)
by A13, XCMPLX_1:90
.=
p2 `2
by A5, TOPRNS_1:25, XCMPLX_1:88
;
then |.|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn))]|.| * (- (sqrt (1 - (((((|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn))]| `2 ) / |.|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn))]|.|) - sn) / (1 - sn)) ^2 )))) =
|.|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn))]|.| * (- (sqrt (1 - (((p2 `2 ) / |.|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn))]|.|) ^2 ))))
by A5, A18, TOPRNS_1:25, XCMPLX_1:90
.=
|.|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn))]|.| * (- (sqrt (1 - (((p2 `2 ) ^2 ) / (|.|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn))]|.| ^2 )))))
by XCMPLX_1:77
.=
|.|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn))]|.| * (- (sqrt (((|.|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn))]|.| ^2 ) / (|.|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn))]|.| ^2 )) - (((p2 `2 ) ^2 ) / (|.|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn))]|.| ^2 )))))
by A10, A17, XCMPLX_1:60
.=
|.|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn))]|.| * (- (sqrt (((|.|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn))]|.| ^2 ) - ((p2 `2 ) ^2 )) / (|.|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn))]|.| ^2 ))))
by XCMPLX_1:121
.=
|.|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn))]|.| * (- (sqrt (((((p2 `1 ) ^2 ) + ((p2 `2 ) ^2 )) - ((p2 `2 ) ^2 )) / (|.|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn))]|.| ^2 ))))
by A17, JGRAPH_3:10
.=
|.|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 - sn)) + sn))]|.| * (- (sqrt (((p2 `1 ) / |.p2.|) ^2 )))
by A18, XCMPLX_1:77
;
hence
ex
x being
set st
(
x in dom (sn -FanMorphW ) &
y = (sn -FanMorphW ) . x )
by A20, A22, A21, A12, EUCLID:57;
verum end; case A23:
(
(p2 `2 ) / |.p2.| < 0 &
p2 `1 <= 0 &
p2 <> 0. (TOP-REAL 2) )
;
ex x being set st
( x in dom (sn -FanMorphW ) & y = (sn -FanMorphW ) . x )A24:
1
+ sn >= 0
by A1, XREAL_1:150;
then
((p2 `2 ) / |.p2.|) * (1 + sn) <= 0
by A23;
then
1
- sn >= ((p2 `2 ) / |.p2.|) * (1 + sn)
by A2, XREAL_1:151;
then A25:
(1 - sn) + sn >= (((p2 `2 ) / |.p2.|) * (1 + sn)) + sn
by XREAL_1:9;
set px =
|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn))]|;
A26:
|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn))]| `2 = |.p2.| * ((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn)
by EUCLID:56;
|.p2.| <> 0
by A23, TOPRNS_1:25;
then A27:
|.p2.| ^2 > 0
by SQUARE_1:74;
A28:
|.p2.| > 0
by A23, Lm1;
A29:
dom (sn -FanMorphW ) = the
carrier of
(TOP-REAL 2)
by FUNCT_2:def 1;
A30:
1
+ sn > 0
by A1, XREAL_1:150;
0 <= (p2 `1 ) ^2
by XREAL_1:65;
then
(
|.p2.| ^2 = ((p2 `1 ) ^2 ) + ((p2 `2 ) ^2 ) &
0 + ((p2 `2 ) ^2 ) <= ((p2 `1 ) ^2 ) + ((p2 `2 ) ^2 ) )
by JGRAPH_3:10, XREAL_1:9;
then
((p2 `2 ) ^2 ) / (|.p2.| ^2 ) <= (|.p2.| ^2 ) / (|.p2.| ^2 )
by XREAL_1:74;
then
((p2 `2 ) ^2 ) / (|.p2.| ^2 ) <= 1
by A27, XCMPLX_1:60;
then
((p2 `2 ) / |.p2.|) ^2 <= 1
by XCMPLX_1:77;
then
(p2 `2 ) / |.p2.| >= - 1
by SQUARE_1:121;
then
((p2 `2 ) / |.p2.|) * (1 + sn) >= (- 1) * (1 + sn)
by A30, XREAL_1:66;
then
((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn) - sn >= (- 1) - sn
;
then
(((p2 `2 ) / |.p2.|) * (1 + sn)) + sn >= - 1
by XREAL_1:11;
then
1
^2 >= ((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn) ^2
by A25, SQUARE_1:119;
then A31:
1
- (((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn) ^2 ) >= 0
by XREAL_1:50;
then A32:
sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn) ^2 )) >= 0
by SQUARE_1:def 4;
A33:
|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn))]| `1 = - (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn) ^2 ))))
by EUCLID:56;
then |.|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn))]|.| ^2 =
((- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn) ^2 ))))) ^2 ) + ((|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn)) ^2 )
by A26, JGRAPH_3:10
.=
((|.p2.| ^2 ) * ((sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn) ^2 ))) ^2 )) + ((|.p2.| ^2 ) * (((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn) ^2 ))
;
then A34:
|.|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn))]|.| ^2 =
((|.p2.| ^2 ) * (1 - (((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn) ^2 ))) + ((|.p2.| ^2 ) * (((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn) ^2 ))
by A31, SQUARE_1:def 4
.=
|.p2.| ^2
;
then A35:
|.|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn))]|.| =
sqrt (|.p2.| ^2 )
by SQUARE_1:89
.=
|.p2.|
by SQUARE_1:89
;
then A36:
|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn))]| <> 0. (TOP-REAL 2)
by A23, TOPRNS_1:24, TOPRNS_1:25;
(((p2 `2 ) / |.p2.|) * (1 + sn)) + sn <= 0 + sn
by A23, A24, XREAL_1:9;
then
(|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn))]| `2 ) / |.|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn))]|.| <= sn
by A23, A26, A35, TOPRNS_1:25, XCMPLX_1:90;
then A37:
(sn -FanMorphW ) . |[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn))]| = |[(|.|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn))]|.| * (- (sqrt (1 - (((((|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn))]| `2 ) / |.|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn))]|.|) - sn) / (1 + sn)) ^2 ))))),(|.|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn))]|.| * ((((|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn))]| `2 ) / |.|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn))]|.|) - sn) / (1 + sn)))]|
by A1, A2, A33, A32, A36, Th25;
A38:
|.|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn))]|.| * (- (sqrt (((p2 `1 ) / |.p2.|) ^2 ))) =
|.|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn))]|.| * (- (- ((p2 `1 ) / |.p2.|)))
by A23, SQUARE_1:90
.=
p2 `1
by A28, A35, XCMPLX_1:88
;
A39:
|.|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn))]|.| * ((((|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn))]| `2 ) / |.|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn))]|.|) - sn) / (1 + sn)) =
|.p2.| * ((((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn) - sn) / (1 + sn))
by A23, A26, A35, TOPRNS_1:25, XCMPLX_1:90
.=
|.p2.| * ((p2 `2 ) / |.p2.|)
by A30, XCMPLX_1:90
.=
p2 `2
by A23, TOPRNS_1:25, XCMPLX_1:88
;
then |.|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn))]|.| * (- (sqrt (1 - (((((|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn))]| `2 ) / |.|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn))]|.|) - sn) / (1 + sn)) ^2 )))) =
|.|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn))]|.| * (- (sqrt (1 - (((p2 `2 ) / |.|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn))]|.|) ^2 ))))
by A23, A35, TOPRNS_1:25, XCMPLX_1:90
.=
|.|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn))]|.| * (- (sqrt (1 - (((p2 `2 ) ^2 ) / (|.|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn))]|.| ^2 )))))
by XCMPLX_1:77
.=
|.|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn))]|.| * (- (sqrt (((|.|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn))]|.| ^2 ) / (|.|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn))]|.| ^2 )) - (((p2 `2 ) ^2 ) / (|.|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn))]|.| ^2 )))))
by A27, A34, XCMPLX_1:60
.=
|.|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn))]|.| * (- (sqrt (((|.|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn))]|.| ^2 ) - ((p2 `2 ) ^2 )) / (|.|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn))]|.| ^2 ))))
by XCMPLX_1:121
.=
|.|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn))]|.| * (- (sqrt (((((p2 `1 ) ^2 ) + ((p2 `2 ) ^2 )) - ((p2 `2 ) ^2 )) / (|.|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn))]|.| ^2 ))))
by A34, JGRAPH_3:10
.=
|.|[(- (|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn) ^2 ))))),(|.p2.| * ((((p2 `2 ) / |.p2.|) * (1 + sn)) + sn))]|.| * (- (sqrt (((p2 `1 ) / |.p2.|) ^2 )))
by A35, XCMPLX_1:77
;
hence
ex
x being
set st
(
x in dom (sn -FanMorphW ) &
y = (sn -FanMorphW ) . x )
by A37, A39, A38, A29, EUCLID:57;
verum end;
hence
y in rng f
by A3, FUNCT_1:def 5;
verum
end;
hence
rng (sn -FanMorphW ) = the
carrier of
(TOP-REAL 2)
by A3, XBOOLE_0:def 10;
verum
end;
hence
rng (sn -FanMorphW ) = the carrier of (TOP-REAL 2)
; verum