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