let sn be Real; :: thesis: for K0, B0 being Subset of (TOP-REAL 2)
for f being Function of ((TOP-REAL 2) | K0),((TOP-REAL 2) | B0) st - 1 < sn & sn < 1 & f = (sn -FanMorphE) | K0 & B0 = { q where q is Point of (TOP-REAL 2) : ( q `1 >= 0 & q <> 0. (TOP-REAL 2) ) } & K0 = { p where p is Point of (TOP-REAL 2) : ( (p `2) / |.p.| <= sn & p `1 >= 0 & p <> 0. (TOP-REAL 2) ) } holds
f is continuous
let K0, B0 be Subset of (TOP-REAL 2); :: thesis: for f being Function of ((TOP-REAL 2) | K0),((TOP-REAL 2) | B0) st - 1 < sn & sn < 1 & f = (sn -FanMorphE) | K0 & B0 = { q where q is Point of (TOP-REAL 2) : ( q `1 >= 0 & q <> 0. (TOP-REAL 2) ) } & K0 = { p where p is Point of (TOP-REAL 2) : ( (p `2) / |.p.| <= sn & p `1 >= 0 & p <> 0. (TOP-REAL 2) ) } holds
f is continuous
let f be Function of ((TOP-REAL 2) | K0),((TOP-REAL 2) | B0); :: thesis: ( - 1 < sn & sn < 1 & f = (sn -FanMorphE) | K0 & B0 = { q where q is Point of (TOP-REAL 2) : ( q `1 >= 0 & q <> 0. (TOP-REAL 2) ) } & K0 = { p where p is Point of (TOP-REAL 2) : ( (p `2) / |.p.| <= sn & p `1 >= 0 & p <> 0. (TOP-REAL 2) ) } implies f is continuous )
set cn = sqrt (1 - (sn ^2));
set p0 = |[(sqrt (1 - (sn ^2))),sn]|;
A1: |[(sqrt (1 - (sn ^2))),sn]| `1 = sqrt (1 - (sn ^2)) by EUCLID:52;
|[(sqrt (1 - (sn ^2))),sn]| `2 = sn by EUCLID:52;
then A2: |.|[(sqrt (1 - (sn ^2))),sn]|.| = sqrt (((sqrt (1 - (sn ^2))) ^2) + (sn ^2)) by A1, JGRAPH_3:1;
assume A3: ( - 1 < sn & sn < 1 & f = (sn -FanMorphE) | K0 & B0 = { q where q is Point of (TOP-REAL 2) : ( q `1 >= 0 & q <> 0. (TOP-REAL 2) ) } & K0 = { p where p is Point of (TOP-REAL 2) : ( (p `2) / |.p.| <= sn & p `1 >= 0 & p <> 0. (TOP-REAL 2) ) } ) ; :: thesis: f is continuous
then sn ^2 < 1 ^2 by SQUARE_1:50;
then A4: 1 - (sn ^2) > 0 by XREAL_1:50;
then A5: - (- (sqrt (1 - (sn ^2)))) > 0 by SQUARE_1:25;
(sqrt (1 - (sn ^2))) ^2 = 1 - (sn ^2) by A4, SQUARE_1:def 2;
then (|[(sqrt (1 - (sn ^2))),sn]| `2) / |.|[(sqrt (1 - (sn ^2))),sn]|.| = sn by A2, EUCLID:52, SQUARE_1:18;
then A6: |[(sqrt (1 - (sn ^2))),sn]| in K0 by A3, A1, A5, JGRAPH_2:3;
then reconsider K1 = K0 as non empty Subset of (TOP-REAL 2) ;
A7: rng (proj1 * ((sn -FanMorphE) | K1)) c= the carrier of R^1 by TOPMETR:17;
A8: K0 c= B0
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in K0 or x in B0 )
assume x in K0 ; :: thesis: x in B0
then ex p8 being Point of (TOP-REAL 2) st
( x = p8 & (p8 `2) / |.p8.| <= sn & p8 `1 >= 0 & p8 <> 0. (TOP-REAL 2) ) by A3;
hence x in B0 by A3; :: thesis: verum
end;
A9: dom ((sn -FanMorphE) | K1) c= dom (proj2 * ((sn -FanMorphE) | K1))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom ((sn -FanMorphE) | K1) or x in dom (proj2 * ((sn -FanMorphE) | K1)) )
assume A10: x in dom ((sn -FanMorphE) | K1) ; :: thesis: x in dom (proj2 * ((sn -FanMorphE) | K1))
then x in (dom (sn -FanMorphE)) /\ K1 by RELAT_1:61;
then x in dom (sn -FanMorphE) by XBOOLE_0:def 4;
then A11: ( dom proj2 = the carrier of (TOP-REAL 2) & (sn -FanMorphE) . x in rng (sn -FanMorphE) ) by FUNCT_1:3, FUNCT_2:def 1;
((sn -FanMorphE) | K1) . x = (sn -FanMorphE) . x by A10, FUNCT_1:47;
hence x in dom (proj2 * ((sn -FanMorphE) | K1)) by A10, A11, FUNCT_1:11; :: thesis: verum
end;
A12: rng (proj2 * ((sn -FanMorphE) | K1)) c= the carrier of R^1 by TOPMETR:17;
dom (proj2 * ((sn -FanMorphE) | K1)) c= dom ((sn -FanMorphE) | K1) by RELAT_1:25;
then dom (proj2 * ((sn -FanMorphE) | K1)) = dom ((sn -FanMorphE) | K1) by A9, XBOOLE_0:def 10
.= (dom (sn -FanMorphE)) /\ K1 by RELAT_1:61
.= the carrier of (TOP-REAL 2) /\ K1 by FUNCT_2:def 1
.= K1 by XBOOLE_1:28
.= the carrier of ((TOP-REAL 2) | K1) by PRE_TOPC:8 ;
then reconsider g2 = proj2 * ((sn -FanMorphE) | K1) as Function of ((TOP-REAL 2) | K1),R^1 by A12, FUNCT_2:2;
for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds
g2 . p = |.p.| * ((((p `2) / |.p.|) - sn) / (1 + sn))
proof
let p be Point of (TOP-REAL 2); :: thesis: ( p in the carrier of ((TOP-REAL 2) | K1) implies g2 . p = |.p.| * ((((p `2) / |.p.|) - sn) / (1 + sn)) )
A13: dom ((sn -FanMorphE) | K1) = (dom (sn -FanMorphE)) /\ K1 by RELAT_1:61
.= the carrier of (TOP-REAL 2) /\ K1 by FUNCT_2:def 1
.= K1 by XBOOLE_1:28 ;
A14: the carrier of ((TOP-REAL 2) | K1) = K1 by PRE_TOPC:8;
assume A15: p in the carrier of ((TOP-REAL 2) | K1) ; :: thesis: g2 . p = |.p.| * ((((p `2) / |.p.|) - sn) / (1 + sn))
then ex p3 being Point of (TOP-REAL 2) st
( p = p3 & (p3 `2) / |.p3.| <= sn & p3 `1 >= 0 & p3 <> 0. (TOP-REAL 2) ) by A3, A14;
then A16: (sn -FanMorphE) . p = |[(|.p.| * (sqrt (1 - (((((p `2) / |.p.|) - sn) / (1 + sn)) ^2)))),(|.p.| * ((((p `2) / |.p.|) - sn) / (1 + sn)))]| by A3, Th84;
((sn -FanMorphE) | K1) . p = (sn -FanMorphE) . p by A15, A14, FUNCT_1:49;
then g2 . p = proj2 . |[(|.p.| * (sqrt (1 - (((((p `2) / |.p.|) - sn) / (1 + sn)) ^2)))),(|.p.| * ((((p `2) / |.p.|) - sn) / (1 + sn)))]| by A15, A13, A14, A16, FUNCT_1:13
.= |[(|.p.| * (sqrt (1 - (((((p `2) / |.p.|) - sn) / (1 + sn)) ^2)))),(|.p.| * ((((p `2) / |.p.|) - sn) / (1 + sn)))]| `2 by PSCOMP_1:def 6
.= |.p.| * ((((p `2) / |.p.|) - sn) / (1 + sn)) by EUCLID:52 ;
hence g2 . p = |.p.| * ((((p `2) / |.p.|) - sn) / (1 + sn)) ; :: thesis: verum
end;
then consider f2 being Function of ((TOP-REAL 2) | K1),R^1 such that
A17: for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds
f2 . p = |.p.| * ((((p `2) / |.p.|) - sn) / (1 + sn)) ;
A18: dom ((sn -FanMorphE) | K1) c= dom (proj1 * ((sn -FanMorphE) | K1))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom ((sn -FanMorphE) | K1) or x in dom (proj1 * ((sn -FanMorphE) | K1)) )
assume A19: x in dom ((sn -FanMorphE) | K1) ; :: thesis: x in dom (proj1 * ((sn -FanMorphE) | K1))
then x in (dom (sn -FanMorphE)) /\ K1 by RELAT_1:61;
then x in dom (sn -FanMorphE) by XBOOLE_0:def 4;
then A20: ( dom proj1 = the carrier of (TOP-REAL 2) & (sn -FanMorphE) . x in rng (sn -FanMorphE) ) by FUNCT_1:3, FUNCT_2:def 1;
((sn -FanMorphE) | K1) . x = (sn -FanMorphE) . x by A19, FUNCT_1:47;
hence x in dom (proj1 * ((sn -FanMorphE) | K1)) by A19, A20, FUNCT_1:11; :: thesis: verum
end;
dom (proj1 * ((sn -FanMorphE) | K1)) c= dom ((sn -FanMorphE) | K1) by RELAT_1:25;
then dom (proj1 * ((sn -FanMorphE) | K1)) = dom ((sn -FanMorphE) | K1) by A18, XBOOLE_0:def 10
.= (dom (sn -FanMorphE)) /\ K1 by RELAT_1:61
.= the carrier of (TOP-REAL 2) /\ K1 by FUNCT_2:def 1
.= K1 by XBOOLE_1:28
.= the carrier of ((TOP-REAL 2) | K1) by PRE_TOPC:8 ;
then reconsider g1 = proj1 * ((sn -FanMorphE) | K1) as Function of ((TOP-REAL 2) | K1),R^1 by A7, FUNCT_2:2;
for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds
g1 . p = |.p.| * (sqrt (1 - (((((p `2) / |.p.|) - sn) / (1 + sn)) ^2)))
proof
let p be Point of (TOP-REAL 2); :: thesis: ( p in the carrier of ((TOP-REAL 2) | K1) implies g1 . p = |.p.| * (sqrt (1 - (((((p `2) / |.p.|) - sn) / (1 + sn)) ^2))) )
A21: dom ((sn -FanMorphE) | K1) = (dom (sn -FanMorphE)) /\ K1 by RELAT_1:61
.= the carrier of (TOP-REAL 2) /\ K1 by FUNCT_2:def 1
.= K1 by XBOOLE_1:28 ;
A22: the carrier of ((TOP-REAL 2) | K1) = K1 by PRE_TOPC:8;
assume A23: p in the carrier of ((TOP-REAL 2) | K1) ; :: thesis: g1 . p = |.p.| * (sqrt (1 - (((((p `2) / |.p.|) - sn) / (1 + sn)) ^2)))
then ex p3 being Point of (TOP-REAL 2) st
( p = p3 & (p3 `2) / |.p3.| <= sn & p3 `1 >= 0 & p3 <> 0. (TOP-REAL 2) ) by A3, A22;
then A24: (sn -FanMorphE) . p = |[(|.p.| * (sqrt (1 - (((((p `2) / |.p.|) - sn) / (1 + sn)) ^2)))),(|.p.| * ((((p `2) / |.p.|) - sn) / (1 + sn)))]| by A3, Th84;
((sn -FanMorphE) | K1) . p = (sn -FanMorphE) . p by A23, A22, FUNCT_1:49;
then g1 . p = proj1 . |[(|.p.| * (sqrt (1 - (((((p `2) / |.p.|) - sn) / (1 + sn)) ^2)))),(|.p.| * ((((p `2) / |.p.|) - sn) / (1 + sn)))]| by A23, A21, A22, A24, FUNCT_1:13
.= |[(|.p.| * (sqrt (1 - (((((p `2) / |.p.|) - sn) / (1 + sn)) ^2)))),(|.p.| * ((((p `2) / |.p.|) - sn) / (1 + sn)))]| `1 by PSCOMP_1:def 5
.= |.p.| * (sqrt (1 - (((((p `2) / |.p.|) - sn) / (1 + sn)) ^2))) by EUCLID:52 ;
hence g1 . p = |.p.| * (sqrt (1 - (((((p `2) / |.p.|) - sn) / (1 + sn)) ^2))) ; :: thesis: verum
end;
then consider f1 being Function of ((TOP-REAL 2) | K1),R^1 such that
A25: for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds
f1 . p = |.p.| * (sqrt (1 - (((((p `2) / |.p.|) - sn) / (1 + sn)) ^2))) ;
for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K1) holds
( q `1 >= 0 & (q `2) / |.q.| <= sn & q <> 0. (TOP-REAL 2) )
proof
let q be Point of (TOP-REAL 2); :: thesis: ( q in the carrier of ((TOP-REAL 2) | K1) implies ( q `1 >= 0 & (q `2) / |.q.| <= sn & q <> 0. (TOP-REAL 2) ) )
A26: the carrier of ((TOP-REAL 2) | K1) = K1 by PRE_TOPC:8;
assume q in the carrier of ((TOP-REAL 2) | K1) ; :: thesis: ( q `1 >= 0 & (q `2) / |.q.| <= sn & q <> 0. (TOP-REAL 2) )
then ex p3 being Point of (TOP-REAL 2) st
( q = p3 & (p3 `2) / |.p3.| <= sn & p3 `1 >= 0 & p3 <> 0. (TOP-REAL 2) ) by A3, A26;
hence ( q `1 >= 0 & (q `2) / |.q.| <= sn & q <> 0. (TOP-REAL 2) ) ; :: thesis: verum
end;
then A27: f1 is continuous by A3, A25, Th88;
A28: for x, y, r, s being Real st |[x,y]| in K1 & r = f1 . |[x,y]| & s = f2 . |[x,y]| holds
f . |[x,y]| = |[r,s]|
proof
let x, y, r, s be Real; :: thesis: ( |[x,y]| in K1 & r = f1 . |[x,y]| & s = f2 . |[x,y]| implies f . |[x,y]| = |[r,s]| )
assume that
A29: |[x,y]| in K1 and
A30: ( r = f1 . |[x,y]| & s = f2 . |[x,y]| ) ; :: thesis: f . |[x,y]| = |[r,s]|
set p99 = |[x,y]|;
A31: ex p3 being Point of (TOP-REAL 2) st
( |[x,y]| = p3 & (p3 `2) / |.p3.| <= sn & p3 `1 >= 0 & p3 <> 0. (TOP-REAL 2) ) by A3, A29;
A32: the carrier of ((TOP-REAL 2) | K1) = K1 by PRE_TOPC:8;
then A33: f1 . |[x,y]| = |.|[x,y]|.| * (sqrt (1 - (((((|[x,y]| `2) / |.|[x,y]|.|) - sn) / (1 + sn)) ^2))) by A25, A29;
((sn -FanMorphE) | K0) . |[x,y]| = (sn -FanMorphE) . |[x,y]| by A29, FUNCT_1:49
.= |[(|.|[x,y]|.| * (sqrt (1 - (((((|[x,y]| `2) / |.|[x,y]|.|) - sn) / (1 + sn)) ^2)))),(|.|[x,y]|.| * ((((|[x,y]| `2) / |.|[x,y]|.|) - sn) / (1 + sn)))]| by A3, A31, Th84
.= |[r,s]| by A17, A29, A30, A32, A33 ;
hence f . |[x,y]| = |[r,s]| by A3; :: thesis: verum
end;
for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K1) holds
( q `1 >= 0 & q <> 0. (TOP-REAL 2) )
proof
let q be Point of (TOP-REAL 2); :: thesis: ( q in the carrier of ((TOP-REAL 2) | K1) implies ( q `1 >= 0 & q <> 0. (TOP-REAL 2) ) )
A34: the carrier of ((TOP-REAL 2) | K1) = K1 by PRE_TOPC:8;
assume q in the carrier of ((TOP-REAL 2) | K1) ; :: thesis: ( q `1 >= 0 & q <> 0. (TOP-REAL 2) )
then ex p3 being Point of (TOP-REAL 2) st
( q = p3 & (p3 `2) / |.p3.| <= sn & p3 `1 >= 0 & p3 <> 0. (TOP-REAL 2) ) by A3, A34;
hence ( q `1 >= 0 & q <> 0. (TOP-REAL 2) ) ; :: thesis: verum
end;
then f2 is continuous by A3, A17, Th86;
hence f is continuous by A6, A8, A27, A28, JGRAPH_2:35; :: thesis: verum