let cn be Real; ( - 1 < cn & cn < 1 implies ( cn -FanMorphS is Function of (TOP-REAL 2),(TOP-REAL 2) & rng (cn -FanMorphS) = the carrier of (TOP-REAL 2) ) )
assume that
A1:
- 1 < cn
and
A2:
cn < 1
; ( cn -FanMorphS is Function of (TOP-REAL 2),(TOP-REAL 2) & rng (cn -FanMorphS) = the carrier of (TOP-REAL 2) )
thus
cn -FanMorphS is Function of (TOP-REAL 2),(TOP-REAL 2)
; rng (cn -FanMorphS) = the carrier of (TOP-REAL 2)
for f being Function of (TOP-REAL 2),(TOP-REAL 2) st f = cn -FanMorphS holds
rng (cn -FanMorphS) = the carrier of (TOP-REAL 2)
proof
let f be
Function of
(TOP-REAL 2),
(TOP-REAL 2);
( f = cn -FanMorphS implies rng (cn -FanMorphS) = the carrier of (TOP-REAL 2) )
assume A3:
f = cn -FanMorphS
;
rng (cn -FanMorphS) = 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
object ;
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 ( ( p2 `2 >= 0 & ex x being set st
( x in dom (cn -FanMorphS) & y = (cn -FanMorphS) . x ) ) or ( (p2 `1) / |.p2.| >= 0 & p2 `2 <= 0 & p2 <> 0. (TOP-REAL 2) & ex x being set st
( x in dom (cn -FanMorphS) & y = (cn -FanMorphS) . x ) ) or ( (p2 `1) / |.p2.| < 0 & p2 `2 <= 0 & p2 <> 0. (TOP-REAL 2) & ex x being set st
( x in dom (cn -FanMorphS) & y = (cn -FanMorphS) . x ) ) )per cases
( p2 `2 >= 0 or ( (p2 `1) / |.p2.| >= 0 & p2 `2 <= 0 & p2 <> 0. (TOP-REAL 2) ) or ( (p2 `1) / |.p2.| < 0 & p2 `2 <= 0 & p2 <> 0. (TOP-REAL 2) ) )
by JGRAPH_2:3;
case A5:
(
(p2 `1) / |.p2.| >= 0 &
p2 `2 <= 0 &
p2 <> 0. (TOP-REAL 2) )
;
ex x being set st
( x in dom (cn -FanMorphS) & y = (cn -FanMorphS) . x )
- (- (1 + cn)) > 0
by A1, XREAL_1:148;
then A6:
- ((- 1) - cn) > 0
;
A7:
1
- cn >= 0
by A2, XREAL_1:149;
then
((p2 `1) / |.p2.|) * (1 - cn) >= 0
by A5;
then
(- 1) - cn <= ((p2 `1) / |.p2.|) * (1 - cn)
by A6;
then A8:
((- 1) - cn) + cn <= (((p2 `1) / |.p2.|) * (1 - cn)) + cn
by XREAL_1:7;
set px =
|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 - cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 - cn)) + cn) ^2)))))]|;
A9:
|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 - cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 - cn)) + cn) ^2)))))]| `1 = |.p2.| * ((((p2 `1) / |.p2.|) * (1 - cn)) + cn)
by EUCLID:52;
|.p2.| <> 0
by A5, TOPRNS_1:24;
then A10:
|.p2.| ^2 > 0
by SQUARE_1:12;
A11:
dom (cn -FanMorphS) = the
carrier of
(TOP-REAL 2)
by FUNCT_2:def 1;
A12:
1
- cn > 0
by A2, XREAL_1:149;
0 <= (p2 `2) ^2
by XREAL_1:63;
then
(
|.p2.| ^2 = ((p2 `1) ^2) + ((p2 `2) ^2) &
0 + ((p2 `1) ^2) <= ((p2 `1) ^2) + ((p2 `2) ^2) )
by JGRAPH_3:1, XREAL_1:7;
then
((p2 `1) ^2) / (|.p2.| ^2) <= (|.p2.| ^2) / (|.p2.| ^2)
by XREAL_1:72;
then
((p2 `1) ^2) / (|.p2.| ^2) <= 1
by A10, XCMPLX_1:60;
then
((p2 `1) / |.p2.|) ^2 <= 1
by XCMPLX_1:76;
then
(p2 `1) / |.p2.| <= 1
by SQUARE_1:51;
then
((p2 `1) / |.p2.|) * (1 - cn) <= 1
* (1 - cn)
by A12, XREAL_1:64;
then
((((p2 `1) / |.p2.|) * (1 - cn)) + cn) - cn <= 1
- cn
;
then
(((p2 `1) / |.p2.|) * (1 - cn)) + cn <= 1
by XREAL_1:9;
then
1
^2 >= ((((p2 `1) / |.p2.|) * (1 - cn)) + cn) ^2
by A8, SQUARE_1:49;
then A13:
1
- (((((p2 `1) / |.p2.|) * (1 - cn)) + cn) ^2) >= 0
by XREAL_1:48;
then A14:
sqrt (1 - (((((p2 `1) / |.p2.|) * (1 - cn)) + cn) ^2)) >= 0
by SQUARE_1:def 2;
A15:
|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 - cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 - cn)) + cn) ^2)))))]| `2 = - (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 - cn)) + cn) ^2))))
by EUCLID:52;
then |.|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 - cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 - cn)) + cn) ^2)))))]|.| ^2 =
(((- |.p2.|) * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 - cn)) + cn) ^2)))) ^2) + ((|.p2.| * ((((p2 `1) / |.p2.|) * (1 - cn)) + cn)) ^2)
by A9, JGRAPH_3:1
.=
((|.p2.| ^2) * ((sqrt (1 - (((((p2 `1) / |.p2.|) * (1 - cn)) + cn) ^2))) ^2)) + ((|.p2.| ^2) * (((((p2 `1) / |.p2.|) * (1 - cn)) + cn) ^2))
;
then A16:
|.|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 - cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 - cn)) + cn) ^2)))))]|.| ^2 =
((|.p2.| ^2) * (1 - (((((p2 `1) / |.p2.|) * (1 - cn)) + cn) ^2))) + ((|.p2.| ^2) * (((((p2 `1) / |.p2.|) * (1 - cn)) + cn) ^2))
by A13, SQUARE_1:def 2
.=
|.p2.| ^2
;
then A17:
|.|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 - cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 - cn)) + cn) ^2)))))]|.| =
sqrt (|.p2.| ^2)
by SQUARE_1:22
.=
|.p2.|
by SQUARE_1:22
;
then A18:
|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 - cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 - cn)) + cn) ^2)))))]| <> 0. (TOP-REAL 2)
by A5, TOPRNS_1:23, TOPRNS_1:24;
(((p2 `1) / |.p2.|) * (1 - cn)) + cn >= 0 + cn
by A5, A7, XREAL_1:7;
then
(|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 - cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 - cn)) + cn) ^2)))))]| `1) / |.|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 - cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 - cn)) + cn) ^2)))))]|.| >= cn
by A5, A9, A17, TOPRNS_1:24, XCMPLX_1:89;
then A19:
(cn -FanMorphS) . |[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 - cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 - cn)) + cn) ^2)))))]| = |[(|.|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 - cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 - cn)) + cn) ^2)))))]|.| * ((((|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 - cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 - cn)) + cn) ^2)))))]| `1) / |.|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 - cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 - cn)) + cn) ^2)))))]|.|) - cn) / (1 - cn))),(|.|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 - cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 - cn)) + cn) ^2)))))]|.| * (- (sqrt (1 - (((((|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 - cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 - cn)) + cn) ^2)))))]| `1) / |.|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 - cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 - cn)) + cn) ^2)))))]|.|) - cn) / (1 - cn)) ^2)))))]|
by A1, A2, A15, A14, A18, Th115;
|.|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 - cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 - cn)) + cn) ^2)))))]|.| * (sqrt ((- ((p2 `2) / |.p2.|)) ^2)) =
|.p2.| * (- ((p2 `2) / |.p2.|))
by A5, A17, SQUARE_1:22
.=
((- (p2 `2)) / |.p2.|) * |.p2.|
by XCMPLX_1:187
.=
- (p2 `2)
by A5, TOPRNS_1:24, XCMPLX_1:87
;
then A20:
|.|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 - cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 - cn)) + cn) ^2)))))]|.| * (- (sqrt ((- ((p2 `2) / |.p2.|)) ^2))) = p2 `2
;
A21:
|.|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 - cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 - cn)) + cn) ^2)))))]|.| * ((((|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 - cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 - cn)) + cn) ^2)))))]| `1) / |.|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 - cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 - cn)) + cn) ^2)))))]|.|) - cn) / (1 - cn)) =
|.p2.| * ((((((p2 `1) / |.p2.|) * (1 - cn)) + cn) - cn) / (1 - cn))
by A5, A9, A17, TOPRNS_1:24, XCMPLX_1:89
.=
|.p2.| * ((p2 `1) / |.p2.|)
by A12, XCMPLX_1:89
.=
p2 `1
by A5, TOPRNS_1:24, XCMPLX_1:87
;
then |.|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 - cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 - cn)) + cn) ^2)))))]|.| * (- (sqrt (1 - (((((|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 - cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 - cn)) + cn) ^2)))))]| `1) / |.|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 - cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 - cn)) + cn) ^2)))))]|.|) - cn) / (1 - cn)) ^2)))) =
|.|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 - cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 - cn)) + cn) ^2)))))]|.| * (- (sqrt (1 - (((p2 `1) / |.|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 - cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 - cn)) + cn) ^2)))))]|.|) ^2))))
by A5, A17, TOPRNS_1:24, XCMPLX_1:89
.=
|.|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 - cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 - cn)) + cn) ^2)))))]|.| * (- (sqrt (1 - (((p2 `1) ^2) / (|.|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 - cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 - cn)) + cn) ^2)))))]|.| ^2)))))
by XCMPLX_1:76
.=
|.|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 - cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 - cn)) + cn) ^2)))))]|.| * (- (sqrt (((|.|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 - cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 - cn)) + cn) ^2)))))]|.| ^2) / (|.|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 - cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 - cn)) + cn) ^2)))))]|.| ^2)) - (((p2 `1) ^2) / (|.|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 - cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 - cn)) + cn) ^2)))))]|.| ^2)))))
by A10, A16, XCMPLX_1:60
.=
|.|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 - cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 - cn)) + cn) ^2)))))]|.| * (- (sqrt (((|.|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 - cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 - cn)) + cn) ^2)))))]|.| ^2) - ((p2 `1) ^2)) / (|.|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 - cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 - cn)) + cn) ^2)))))]|.| ^2))))
by XCMPLX_1:120
.=
|.|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 - cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 - cn)) + cn) ^2)))))]|.| * (- (sqrt (((((p2 `1) ^2) + ((p2 `2) ^2)) - ((p2 `1) ^2)) / (|.|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 - cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 - cn)) + cn) ^2)))))]|.| ^2))))
by A16, JGRAPH_3:1
.=
|.|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 - cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 - cn)) + cn) ^2)))))]|.| * (- (sqrt (((p2 `2) / |.p2.|) ^2)))
by A17, XCMPLX_1:76
;
hence
ex
x being
set st
(
x in dom (cn -FanMorphS) &
y = (cn -FanMorphS) . x )
by A19, A21, A20, A11, EUCLID:53;
verum end; case A22:
(
(p2 `1) / |.p2.| < 0 &
p2 `2 <= 0 &
p2 <> 0. (TOP-REAL 2) )
;
ex x being set st
( x in dom (cn -FanMorphS) & y = (cn -FanMorphS) . x )A23:
1
+ cn >= 0
by A1, XREAL_1:148;
1
- cn > 0
by A2, XREAL_1:149;
then A24:
(1 - cn) + cn >= (((p2 `1) / |.p2.|) * (1 + cn)) + cn
by A22, A23, XREAL_1:7;
A25:
1
+ cn > 0
by A1, XREAL_1:148;
|.p2.| <> 0
by A22, TOPRNS_1:24;
then A26:
|.p2.| ^2 > 0
by SQUARE_1:12;
0 <= (p2 `2) ^2
by XREAL_1:63;
then
(
|.p2.| ^2 = ((p2 `1) ^2) + ((p2 `2) ^2) &
0 + ((p2 `1) ^2) <= ((p2 `1) ^2) + ((p2 `2) ^2) )
by JGRAPH_3:1, XREAL_1:7;
then
((p2 `1) ^2) / (|.p2.| ^2) <= (|.p2.| ^2) / (|.p2.| ^2)
by XREAL_1:72;
then
((p2 `1) ^2) / (|.p2.| ^2) <= 1
by A26, XCMPLX_1:60;
then
((p2 `1) / |.p2.|) ^2 <= 1
by XCMPLX_1:76;
then
(p2 `1) / |.p2.| >= - 1
by SQUARE_1:51;
then
((p2 `1) / |.p2.|) * (1 + cn) >= (- 1) * (1 + cn)
by A25, XREAL_1:64;
then
((((p2 `1) / |.p2.|) * (1 + cn)) + cn) - cn >= (- 1) - cn
;
then
(((p2 `1) / |.p2.|) * (1 + cn)) + cn >= - 1
by XREAL_1:9;
then
1
^2 >= ((((p2 `1) / |.p2.|) * (1 + cn)) + cn) ^2
by A24, SQUARE_1:49;
then A27:
1
- (((((p2 `1) / |.p2.|) * (1 + cn)) + cn) ^2) >= 0
by XREAL_1:48;
then A28:
sqrt (1 - (((((p2 `1) / |.p2.|) * (1 + cn)) + cn) ^2)) >= 0
by SQUARE_1:def 2;
A29:
dom (cn -FanMorphS) = the
carrier of
(TOP-REAL 2)
by FUNCT_2:def 1;
set px =
|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 + cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 + cn)) + cn) ^2)))))]|;
A30:
|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 + cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 + cn)) + cn) ^2)))))]| `1 = |.p2.| * ((((p2 `1) / |.p2.|) * (1 + cn)) + cn)
by EUCLID:52;
A31:
|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 + cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 + cn)) + cn) ^2)))))]| `2 = - (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 + cn)) + cn) ^2))))
by EUCLID:52;
then |.|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 + cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 + cn)) + cn) ^2)))))]|.| ^2 =
((- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 + cn)) + cn) ^2))))) ^2) + ((|.p2.| * ((((p2 `1) / |.p2.|) * (1 + cn)) + cn)) ^2)
by A30, JGRAPH_3:1
.=
((|.p2.| ^2) * ((sqrt (1 - (((((p2 `1) / |.p2.|) * (1 + cn)) + cn) ^2))) ^2)) + ((|.p2.| ^2) * (((((p2 `1) / |.p2.|) * (1 + cn)) + cn) ^2))
;
then A32:
|.|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 + cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 + cn)) + cn) ^2)))))]|.| ^2 =
((|.p2.| ^2) * (1 - (((((p2 `1) / |.p2.|) * (1 + cn)) + cn) ^2))) + ((|.p2.| ^2) * (((((p2 `1) / |.p2.|) * (1 + cn)) + cn) ^2))
by A27, SQUARE_1:def 2
.=
|.p2.| ^2
;
then A33:
|.|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 + cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 + cn)) + cn) ^2)))))]|.| =
sqrt (|.p2.| ^2)
by SQUARE_1:22
.=
|.p2.|
by SQUARE_1:22
;
then A34:
|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 + cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 + cn)) + cn) ^2)))))]| <> 0. (TOP-REAL 2)
by A22, TOPRNS_1:23, TOPRNS_1:24;
(((p2 `1) / |.p2.|) * (1 + cn)) + cn <= 0 + cn
by A22, A23, XREAL_1:7;
then
(|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 + cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 + cn)) + cn) ^2)))))]| `1) / |.|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 + cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 + cn)) + cn) ^2)))))]|.| <= cn
by A22, A30, A33, TOPRNS_1:24, XCMPLX_1:89;
then A35:
(cn -FanMorphS) . |[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 + cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 + cn)) + cn) ^2)))))]| = |[(|.|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 + cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 + cn)) + cn) ^2)))))]|.| * ((((|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 + cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 + cn)) + cn) ^2)))))]| `1) / |.|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 + cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 + cn)) + cn) ^2)))))]|.|) - cn) / (1 + cn))),(|.|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 + cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 + cn)) + cn) ^2)))))]|.| * (- (sqrt (1 - (((((|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 + cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 + cn)) + cn) ^2)))))]| `1) / |.|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 + cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 + cn)) + cn) ^2)))))]|.|) - cn) / (1 + cn)) ^2)))))]|
by A1, A2, A31, A28, A34, Th115;
A36:
|.|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 + cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 + cn)) + cn) ^2)))))]|.| * (- (sqrt (((p2 `2) / |.p2.|) ^2))) =
|.|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 + cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 + cn)) + cn) ^2)))))]|.| * (- (sqrt ((- ((p2 `2) / |.p2.|)) ^2)))
.=
|.|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 + cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 + cn)) + cn) ^2)))))]|.| * (- (- ((p2 `2) / |.p2.|)))
by A22, SQUARE_1:22
.=
p2 `2
by A22, A33, TOPRNS_1:24, XCMPLX_1:87
;
A37:
|.|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 + cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 + cn)) + cn) ^2)))))]|.| * ((((|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 + cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 + cn)) + cn) ^2)))))]| `1) / |.|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 + cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 + cn)) + cn) ^2)))))]|.|) - cn) / (1 + cn)) =
|.p2.| * ((((((p2 `1) / |.p2.|) * (1 + cn)) + cn) - cn) / (1 + cn))
by A22, A30, A33, TOPRNS_1:24, XCMPLX_1:89
.=
|.p2.| * ((p2 `1) / |.p2.|)
by A25, XCMPLX_1:89
.=
p2 `1
by A22, TOPRNS_1:24, XCMPLX_1:87
;
then |.|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 + cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 + cn)) + cn) ^2)))))]|.| * (- (sqrt (1 - (((((|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 + cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 + cn)) + cn) ^2)))))]| `1) / |.|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 + cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 + cn)) + cn) ^2)))))]|.|) - cn) / (1 + cn)) ^2)))) =
|.|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 + cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 + cn)) + cn) ^2)))))]|.| * (- (sqrt (1 - (((p2 `1) / |.|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 + cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 + cn)) + cn) ^2)))))]|.|) ^2))))
by A22, A33, TOPRNS_1:24, XCMPLX_1:89
.=
|.|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 + cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 + cn)) + cn) ^2)))))]|.| * (- (sqrt (1 - (((p2 `1) ^2) / (|.|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 + cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 + cn)) + cn) ^2)))))]|.| ^2)))))
by XCMPLX_1:76
.=
|.|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 + cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 + cn)) + cn) ^2)))))]|.| * (- (sqrt (((|.|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 + cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 + cn)) + cn) ^2)))))]|.| ^2) / (|.|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 + cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 + cn)) + cn) ^2)))))]|.| ^2)) - (((p2 `1) ^2) / (|.|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 + cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 + cn)) + cn) ^2)))))]|.| ^2)))))
by A26, A32, XCMPLX_1:60
.=
|.|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 + cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 + cn)) + cn) ^2)))))]|.| * (- (sqrt (((|.|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 + cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 + cn)) + cn) ^2)))))]|.| ^2) - ((p2 `1) ^2)) / (|.|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 + cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 + cn)) + cn) ^2)))))]|.| ^2))))
by XCMPLX_1:120
.=
|.|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 + cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 + cn)) + cn) ^2)))))]|.| * (- (sqrt (((((p2 `1) ^2) + ((p2 `2) ^2)) - ((p2 `1) ^2)) / (|.|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 + cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 + cn)) + cn) ^2)))))]|.| ^2))))
by A32, JGRAPH_3:1
.=
|.|[(|.p2.| * ((((p2 `1) / |.p2.|) * (1 + cn)) + cn)),(- (|.p2.| * (sqrt (1 - (((((p2 `1) / |.p2.|) * (1 + cn)) + cn) ^2)))))]|.| * (- (sqrt (((p2 `2) / |.p2.|) ^2)))
by A33, XCMPLX_1:76
;
hence
ex
x being
set st
(
x in dom (cn -FanMorphS) &
y = (cn -FanMorphS) . x )
by A35, A37, A36, A29, EUCLID:53;
verum end;
hence
y in rng f
by A3, FUNCT_1:def 3;
verum
end;
hence
rng (cn -FanMorphS) = the
carrier of
(TOP-REAL 2)
by A3, XBOOLE_0:def 10;
verum
end;
hence
rng (cn -FanMorphS) = the carrier of (TOP-REAL 2)
; verum