let K0, B0 be Subset of (TOP-REAL 2); :: thesis: for f being Function of ((TOP-REAL 2) | K0),((TOP-REAL 2) | B0) st f = Out_In_Sq | K0 & B0 = NonZero (TOP-REAL 2) & K0 = { p where p is Point of (TOP-REAL 2) : ( ( ( p `1 <= p `2 & - (p `2 ) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2 ) ) ) & p <> 0. (TOP-REAL 2) ) } holds
f is continuous
let f be Function of ((TOP-REAL 2) | K0),((TOP-REAL 2) | B0); :: thesis: ( f = Out_In_Sq | K0 & B0 = NonZero (TOP-REAL 2) & K0 = { p where p is Point of (TOP-REAL 2) : ( ( ( p `1 <= p `2 & - (p `2 ) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2 ) ) ) & p <> 0. (TOP-REAL 2) ) } implies f is continuous )
assume A1: ( f = Out_In_Sq | K0 & B0 = NonZero (TOP-REAL 2) & K0 = { p where p is Point of (TOP-REAL 2) : ( ( ( p `1 <= p `2 & - (p `2 ) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2 ) ) ) & p <> 0. (TOP-REAL 2) ) } ) ; :: thesis: f is continuous
( ( ( (1.REAL 2) `1 <= (1.REAL 2) `2 & - ((1.REAL 2) `2 ) <= (1.REAL 2) `1 ) or ( (1.REAL 2) `1 >= (1.REAL 2) `2 & (1.REAL 2) `1 <= - ((1.REAL 2) `2 ) ) ) & 1.REAL 2 <> 0. (TOP-REAL 2) ) by Th13, REVROT_1:19, XX;
then A2: 1.REAL 2 in K0 by A1;
then reconsider K1 = K0 as non empty Subset of (TOP-REAL 2) ;
A3: K0 c= B0

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in K0 or x in B0 )
assume x in K0 ; :: thesis: x in B0
then consider p8 being Point of (TOP-REAL 2) such that
A4: ( x = p8 & ( ( p8 `1 <= p8 `2 & - (p8 `2 ) <= p8 `1 ) or ( p8 `1 >= p8 `2 & p8 `1 <= - (p8 `2 ) ) ) & p8 <> 0. (TOP-REAL 2) ) by A1;
not x in {(0. (TOP-REAL 2))} by A4, TARSKI:def 1;
hence x in B0 by A1, A4, XBOOLE_0:def 5; :: thesis: verum

end;

A5: dom (proj1 * (Out_In_Sq | K1)) c= dom (Out_In_Sq | K1) by RELAT_1:44;
A6: dom (Out_In_Sq | K1) c= dom (proj1 * (Out_In_Sq | K1))

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (Out_In_Sq | K1) or x in dom (proj1 * (Out_In_Sq | K1)) )
assume A7: x in dom (Out_In_Sq | K1) ; :: thesis: x in dom (proj1 * (Out_In_Sq | K1))
then A8: x in (dom Out_In_Sq ) /\ K1 by RELAT_1:90;
A9: (Out_In_Sq | K1) . x = Out_In_Sq . x by A7, FUNCT_1:70;
A10: dom proj1 = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
x in dom Out_In_Sq by A8, XBOOLE_0:def 4;
then Out_In_Sq . x in rng Out_In_Sq by FUNCT_1:12;
then Out_In_Sq . x in the carrier of (TOP-REAL 2) by XBOOLE_0:def 5;
hence x in dom (proj1 * (Out_In_Sq | K1)) by A7, A9, A10, FUNCT_1:21; :: thesis: verum

end;

A11: K1 c= NonZero (TOP-REAL 2)

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in K1 or z in NonZero (TOP-REAL 2) )
assume z in K1 ; :: thesis: z in NonZero (TOP-REAL 2)
then consider p8 being Point of (TOP-REAL 2) such that
A12: ( p8 = z & ( ( p8 `1 <= p8 `2 & - (p8 `2 ) <= p8 `1 ) or ( p8 `1 >= p8 `2 & p8 `1 <= - (p8 `2 ) ) ) & p8 <> 0. (TOP-REAL 2) ) by A1;
( z in the carrier of (TOP-REAL 2) & not z in {(0. (TOP-REAL 2))} ) by A12, TARSKI:def 1;
hence z in NonZero (TOP-REAL 2) by XBOOLE_0:def 5; :: thesis: verum

end;

A13: NonZero (TOP-REAL 2) <> {} by Th19;
A14: dom (proj1 * (Out_In_Sq | K1)) = dom (Out_In_Sq | K1) by A5, A6, XBOOLE_0:def 10
.= (dom Out_In_Sq ) /\ K1 by RELAT_1:90
.= (NonZero (TOP-REAL 2)) /\ K1 by A13, FUNCT_2:def 1
.= K1 by A11, XBOOLE_1:28
.= [#] ((TOP-REAL 2) | K1) by PRE_TOPC:def 10
.= the carrier of ((TOP-REAL 2) | K1) ;
rng (proj1 * (Out_In_Sq | K1)) c= the carrier of R^1 by TOPMETR:24;
then reconsider g2 = proj1 * (Out_In_Sq | K1) as Function of ((TOP-REAL 2) | K1),R^1 by A14, FUNCT_2:4;
A15: dom (proj2 * (Out_In_Sq | K1)) c= dom (Out_In_Sq | K1) by RELAT_1:44;
dom (Out_In_Sq | K1) c= dom (proj2 * (Out_In_Sq | K1))

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (Out_In_Sq | K1) or x in dom (proj2 * (Out_In_Sq | K1)) )
assume A16: x in dom (Out_In_Sq | K1) ; :: thesis: x in dom (proj2 * (Out_In_Sq | K1))
then A17: x in (dom Out_In_Sq ) /\ K1 by RELAT_1:90;
A18: (Out_In_Sq | K1) . x = Out_In_Sq . x by A16, FUNCT_1:70;
A19: dom proj2 = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
x in dom Out_In_Sq by A17, XBOOLE_0:def 4;
then Out_In_Sq . x in rng Out_In_Sq by FUNCT_1:12;
then Out_In_Sq . x in the carrier of (TOP-REAL 2) by XBOOLE_0:def 5;
hence x in dom (proj2 * (Out_In_Sq | K1)) by A16, A18, A19, FUNCT_1:21; :: thesis: verum

end;

then A20: dom (proj2 * (Out_In_Sq | K1)) = dom (Out_In_Sq | K1) by A15, XBOOLE_0:def 10
.= (dom Out_In_Sq ) /\ K1 by RELAT_1:90
.= (NonZero (TOP-REAL 2)) /\ K1 by A13, FUNCT_2:def 1
.= K1 by A11, XBOOLE_1:28
.= [#] ((TOP-REAL 2) | K1) by PRE_TOPC:def 10
.= the carrier of ((TOP-REAL 2) | K1) ;
rng (proj2 * (Out_In_Sq | K1)) c= the carrier of R^1 by TOPMETR:24;
then reconsider g1 = proj2 * (Out_In_Sq | K1) as Function of ((TOP-REAL 2) | K1),R^1 by A20, FUNCT_2:4;
A21: for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K1) holds
q `2 <> 0

proof

let q be Point of (TOP-REAL 2); :: thesis: ( q in the carrier of ((TOP-REAL 2) | K1) implies q `2 <> 0 )
assume A22: q in the carrier of ((TOP-REAL 2) | K1) ; :: thesis: q `2 <> 0
the carrier of ((TOP-REAL 2) | K1) = [#] ((TOP-REAL 2) | K1)
.= K1 by PRE_TOPC:def 10 ;
then consider p3 being Point of (TOP-REAL 2) such that
A23: ( q = p3 & ( ( p3 `1 <= p3 `2 & - (p3 `2 ) <= p3 `1 ) or ( p3 `1 >= p3 `2 & p3 `1 <= - (p3 `2 ) ) ) & p3 <> 0. (TOP-REAL 2) ) by A1, A22;

now

assume A24: q `2 = 0 ; :: thesis: contradiction
then q `1 = 0 by A23;
hence contradiction by A23, A24, EUCLID:57, EUCLID:58; :: thesis: verum

end;

hence q `2 <> 0 ; :: thesis: verum

end;

for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds
g2 . p = ((p `1 ) / (p `2 )) / (p `2 )

proof

let p be Point of (TOP-REAL 2); :: thesis: ( p in the carrier of ((TOP-REAL 2) | K1) implies g2 . p = ((p `1 ) / (p `2 )) / (p `2 ) )
assume A25: p in the carrier of ((TOP-REAL 2) | K1) ; :: thesis: g2 . p = ((p `1 ) / (p `2 )) / (p `2 )
A26: NonZero (TOP-REAL 2) <> {} by Th19;
A27: dom (Out_In_Sq | K1) = (dom Out_In_Sq ) /\ K1 by RELAT_1:90
.= (NonZero (TOP-REAL 2)) /\ K1 by A26, FUNCT_2:def 1
.= K1 by A11, XBOOLE_1:28 ;
A28: the carrier of ((TOP-REAL 2) | K1) = [#] ((TOP-REAL 2) | K1)
.= K1 by PRE_TOPC:def 10 ;
then consider p3 being Point of (TOP-REAL 2) such that
A29: ( p = p3 & ( ( p3 `1 <= p3 `2 & - (p3 `2 ) <= p3 `1 ) or ( p3 `1 >= p3 `2 & p3 `1 <= - (p3 `2 ) ) ) & p3 <> 0. (TOP-REAL 2) ) by A1, A25;
A30: Out_In_Sq . p = |[(((p `1 ) / (p `2 )) / (p `2 )),(1 / (p `2 ))]| by A29, Th24;
(Out_In_Sq | K1) . p = Out_In_Sq . p by A25, A28, FUNCT_1:72;
then g2 . p = proj1 . |[(((p `1 ) / (p `2 )) / (p `2 )),(1 / (p `2 ))]| by A25, A27, A28, A30, FUNCT_1:23
.= |[(((p `1 ) / (p `2 )) / (p `2 )),(1 / (p `2 ))]| `1 by PSCOMP_1:def 28
.= ((p `1 ) / (p `2 )) / (p `2 ) by EUCLID:56 ;
hence g2 . p = ((p `1 ) / (p `2 )) / (p `2 ) ; :: thesis: verum

end;

then consider f2 being Function of ((TOP-REAL 2) | K1),R^1 such that
A31: for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds
f2 . p = ((p `1 ) / (p `2 )) / (p `2 ) ;
A32: f2 is continuous by A21, A31, Th44;
for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds
g1 . p = 1 / (p `2 )

proof

let p be Point of (TOP-REAL 2); :: thesis: ( p in the carrier of ((TOP-REAL 2) | K1) implies g1 . p = 1 / (p `2 ) )
assume A33: p in the carrier of ((TOP-REAL 2) | K1) ; :: thesis: g1 . p = 1 / (p `2 )
A34: K1 c= NonZero (TOP-REAL 2)

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in K1 or z in NonZero (TOP-REAL 2) )
assume z in K1 ; :: thesis: z in NonZero (TOP-REAL 2)
then consider p8 being Point of (TOP-REAL 2) such that
A35: ( p8 = z & ( ( p8 `1 <= p8 `2 & - (p8 `2 ) <= p8 `1 ) or ( p8 `1 >= p8 `2 & p8 `1 <= - (p8 `2 ) ) ) & p8 <> 0. (TOP-REAL 2) ) by A1;
( z in the carrier of (TOP-REAL 2) & not z in {(0. (TOP-REAL 2))} ) by A35, TARSKI:def 1;
hence z in NonZero (TOP-REAL 2) by XBOOLE_0:def 5; :: thesis: verum

end;

A36: NonZero (TOP-REAL 2) <> {} by Th19;
A37: dom (Out_In_Sq | K1) = (dom Out_In_Sq ) /\ K1 by RELAT_1:90
.= (NonZero (TOP-REAL 2)) /\ K1 by A36, FUNCT_2:def 1
.= K1 by A34, XBOOLE_1:28 ;
A38: the carrier of ((TOP-REAL 2) | K1) = [#] ((TOP-REAL 2) | K1)
.= K1 by PRE_TOPC:def 10 ;
then consider p3 being Point of (TOP-REAL 2) such that
A39: ( p = p3 & ( ( p3 `1 <= p3 `2 & - (p3 `2 ) <= p3 `1 ) or ( p3 `1 >= p3 `2 & p3 `1 <= - (p3 `2 ) ) ) & p3 <> 0. (TOP-REAL 2) ) by A1, A33;
A40: Out_In_Sq . p = |[(((p `1 ) / (p `2 )) / (p `2 )),(1 / (p `2 ))]| by A39, Th24;
(Out_In_Sq | K1) . p = Out_In_Sq . p by A33, A38, FUNCT_1:72;
then g1 . p = proj2 . |[(((p `1 ) / (p `2 )) / (p `2 )),(1 / (p `2 ))]| by A33, A37, A38, A40, FUNCT_1:23
.= |[(((p `1 ) / (p `2 )) / (p `2 )),(1 / (p `2 ))]| `2 by PSCOMP_1:def 29
.= 1 / (p `2 ) by EUCLID:56 ;
hence g1 . p = 1 / (p `2 ) ; :: thesis: verum

end;

then consider f1 being Function of ((TOP-REAL 2) | K1),R^1 such that
A41: for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds
f1 . p = 1 / (p `2 ) ;
A42: f1 is continuous by A21, A41, Th42;
for x, y, s, r being real number st |[x,y]| in K1 & s = f2 . |[x,y]| & r = f1 . |[x,y]| holds
f . |[x,y]| = |[s,r]|

proof

let x, y, s, r be real number ; :: thesis: ( |[x,y]| in K1 & s = f2 . |[x,y]| & r = f1 . |[x,y]| implies f . |[x,y]| = |[s,r]| )
assume A43: ( |[x,y]| in K1 & s = f2 . |[x,y]| & r = f1 . |[x,y]| ) ; :: thesis: f . |[x,y]| = |[s,r]|
set p99 = |[x,y]|;
A44: the carrier of ((TOP-REAL 2) | K1) = [#] ((TOP-REAL 2) | K1)
.= K1 by PRE_TOPC:def 10 ;
consider p3 being Point of (TOP-REAL 2) such that
A45: ( |[x,y]| = p3 & ( ( p3 `1 <= p3 `2 & - (p3 `2 ) <= p3 `1 ) or ( p3 `1 >= p3 `2 & p3 `1 <= - (p3 `2 ) ) ) & p3 <> 0. (TOP-REAL 2) ) by A1, A43;
A46: f1 . |[x,y]| = 1 / (|[x,y]| `2 ) by A41, A43, A44;
(Out_In_Sq | K0) . |[x,y]| = Out_In_Sq . |[x,y]| by A43, FUNCT_1:72
.= |[(((|[x,y]| `1 ) / (|[x,y]| `2 )) / (|[x,y]| `2 )),(1 / (|[x,y]| `2 ))]| by A45, Th24
.= |[s,r]| by A31, A43, A44, A46 ;
hence f . |[x,y]| = |[s,r]| by A1; :: thesis: verum

end;

hence f is continuous by A2, A3, A32, A42, Th45; :: thesis: verum