let sn be Real; :: thesis: ( - 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 ; :: thesis: ( 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) ; :: thesis: 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); :: thesis: ( f = sn -FanMorphW implies rng (sn -FanMorphW) = the carrier of (TOP-REAL 2) )
assume A3: f = sn -FanMorphW ; :: thesis: 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 object ; :: 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 :: thesis: ( ( p2 `1 >= 0 & ex x being set st
( x in dom (sn -FanMorphW) & y = (sn -FanMorphW) . x ) ) or ( (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 ) ) or ( (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 ) ) )

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:3;

case p2 `1 >= 0 ; :: thesis: ex x being set st
( x in dom (sn -FanMorphW) & y = (sn -FanMorphW) . x )

then y = (sn -FanMorphW) . p2 by Th16;
hence ex x being set st
( x in dom (sn -FanMorphW) & y = (sn -FanMorphW) . x ) by A3, A4; :: thesis: verum

end;

case A5: ( (p2 `2) / |.p2.| >= 0 & p2 `1 <= 0 & p2 <> 0. (TOP-REAL 2) ) ; :: thesis: ex x being set st
( x in dom (sn -FanMorphW) & y = (sn -FanMorphW) . x )

A6: - (- (1 + sn)) > 0 by A1, XREAL_1:148;
A7: 1 - sn >= 0 by A2, XREAL_1:149;
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:7;
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:52;
|.p2.| <> 0 by A5, TOPRNS_1:24;
then A10: |.p2.| ^2 > 0 by SQUARE_1:12;
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:149;
0 <= (p2 `1) ^2 by XREAL_1:63;
then ( |.p2.| ^2 = ((p2 `1) ^2) + ((p2 `2) ^2) & 0 + ((p2 `2) ^2) <= ((p2 `1) ^2) + ((p2 `2) ^2) ) by JGRAPH_3:1, XREAL_1:7;
then ((p2 `2) ^2) / (|.p2.| ^2) <= (|.p2.| ^2) / (|.p2.| ^2) by XREAL_1:72;
then ((p2 `2) ^2) / (|.p2.| ^2) <= 1 by A10, XCMPLX_1:60;
then ((p2 `2) / |.p2.|) ^2 <= 1 by XCMPLX_1:76;
then (p2 `2) / |.p2.| <= 1 by SQUARE_1:51;
then ((p2 `2) / |.p2.|) * (1 - sn) <= 1 * (1 - sn) by A13, XREAL_1:64;
then ((((p2 `2) / |.p2.|) * (1 - sn)) + sn) - sn <= 1 - sn ;
then (((p2 `2) / |.p2.|) * (1 - sn)) + sn <= 1 by XREAL_1:9;
then 1 ^2 >= ((((p2 `2) / |.p2.|) * (1 - sn)) + sn) ^2 by A8, SQUARE_1:49;
then A14: 1 - (((((p2 `2) / |.p2.|) * (1 - sn)) + sn) ^2) >= 0 by XREAL_1:48;
then A15: sqrt (1 - (((((p2 `2) / |.p2.|) * (1 - sn)) + sn) ^2)) >= 0 by SQUARE_1:def 2;
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:52;
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:1
.= ((|.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 2
.= |.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:22
.= |.p2.| by SQUARE_1:22 ;
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:23, TOPRNS_1:24;
(((p2 `2) / |.p2.|) * (1 - sn)) + sn >= 0 + sn by A5, A7, XREAL_1:7;
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:24, XCMPLX_1:89;
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, Th18;
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:23
.= p2 `1 by A11, A18, XCMPLX_1:87 ;
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:24, XCMPLX_1:89
.= |.p2.| * ((p2 `2) / |.p2.|) by A13, XCMPLX_1:89
.= p2 `2 by A5, TOPRNS_1:24, XCMPLX_1:87 ;
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:24, XCMPLX_1:89
.= |.|[(- (|.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:76
.= |.|[(- (|.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:120
.= |.|[(- (|.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:1
.= |.|[(- (|.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:76 ;
hence ex x being set st
( x in dom (sn -FanMorphW) & y = (sn -FanMorphW) . x ) by A20, A22, A21, A12, EUCLID:53; :: thesis: verum

end;

case A23: ( (p2 `2) / |.p2.| < 0 & p2 `1 <= 0 & p2 <> 0. (TOP-REAL 2) ) ; :: thesis: ex x being set st
( x in dom (sn -FanMorphW) & y = (sn -FanMorphW) . x )

A24: 1 + sn >= 0 by A1, XREAL_1:148;
then ((p2 `2) / |.p2.|) * (1 + sn) <= 0 by A23;
then 1 - sn >= ((p2 `2) / |.p2.|) * (1 + sn) by A2, XREAL_1:149;
then A25: (1 - sn) + sn >= (((p2 `2) / |.p2.|) * (1 + sn)) + sn by XREAL_1:7;
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:52;
|.p2.| <> 0 by A23, TOPRNS_1:24;
then A27: |.p2.| ^2 > 0 by SQUARE_1:12;
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:148;
0 <= (p2 `1) ^2 by XREAL_1:63;
then ( |.p2.| ^2 = ((p2 `1) ^2) + ((p2 `2) ^2) & 0 + ((p2 `2) ^2) <= ((p2 `1) ^2) + ((p2 `2) ^2) ) by JGRAPH_3:1, XREAL_1:7;
then ((p2 `2) ^2) / (|.p2.| ^2) <= (|.p2.| ^2) / (|.p2.| ^2) by XREAL_1:72;
then ((p2 `2) ^2) / (|.p2.| ^2) <= 1 by A27, XCMPLX_1:60;
then ((p2 `2) / |.p2.|) ^2 <= 1 by XCMPLX_1:76;
then (p2 `2) / |.p2.| >= - 1 by SQUARE_1:51;
then ((p2 `2) / |.p2.|) * (1 + sn) >= (- 1) * (1 + sn) by A30, XREAL_1:64;
then ((((p2 `2) / |.p2.|) * (1 + sn)) + sn) - sn >= (- 1) - sn ;
then (((p2 `2) / |.p2.|) * (1 + sn)) + sn >= - 1 by XREAL_1:9;
then 1 ^2 >= ((((p2 `2) / |.p2.|) * (1 + sn)) + sn) ^2 by A25, SQUARE_1:49;
then A31: 1 - (((((p2 `2) / |.p2.|) * (1 + sn)) + sn) ^2) >= 0 by XREAL_1:48;
then A32: sqrt (1 - (((((p2 `2) / |.p2.|) * (1 + sn)) + sn) ^2)) >= 0 by SQUARE_1:def 2;
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:52;
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:1
.= ((|.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 2
.= |.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:22
.= |.p2.| by SQUARE_1:22 ;
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:23, TOPRNS_1:24;
(((p2 `2) / |.p2.|) * (1 + sn)) + sn <= 0 + sn by A23, A24, XREAL_1:7;
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:24, XCMPLX_1:89;
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, Th18;
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:23
.= p2 `1 by A28, A35, XCMPLX_1:87 ;
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:24, XCMPLX_1:89
.= |.p2.| * ((p2 `2) / |.p2.|) by A30, XCMPLX_1:89
.= p2 `2 by A23, TOPRNS_1:24, XCMPLX_1:87 ;
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:24, XCMPLX_1:89
.= |.|[(- (|.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:76
.= |.|[(- (|.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:120
.= |.|[(- (|.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:1
.= |.|[(- (|.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:76 ;
hence ex x being set st
( x in dom (sn -FanMorphW) & y = (sn -FanMorphW) . x ) by A37, A39, A38, A29, EUCLID:53; :: thesis: verum

end;

end;

end;

hence y in rng f by A3, FUNCT_1:def 3; :: thesis: verum

end;

hence rng (sn -FanMorphW) = the carrier of (TOP-REAL 2) by A3, XBOOLE_0:def 10; :: thesis: verum

end;

hence rng (sn -FanMorphW) = the carrier of (TOP-REAL 2) ; :: thesis: verum