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 `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) & 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 `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) & p <> 0. (TOP-REAL 2) ) } implies f is continuous )
A1: 1.REAL 2 <> 0. (TOP-REAL 2) by Lm1, REVROT_1:19;
assume A2: ( f = Out_In_Sq | K0 & B0 = NonZero (TOP-REAL 2) & K0 = { p where p is Point of (TOP-REAL 2) : ( ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) & p <> 0. (TOP-REAL 2) ) } ) ; :: thesis: f is continuous
A3: K0 c= B0

proof

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

end;

( ( (1.REAL 2) `2 <= (1.REAL 2) `1 & - ((1.REAL 2) `1) <= (1.REAL 2) `2 ) or ( (1.REAL 2) `2 >= (1.REAL 2) `1 & (1.REAL 2) `2 <= - ((1.REAL 2) `1) ) ) by Th5;
then A5: 1.REAL 2 in K0 by A2, A1;
then reconsider K1 = K0 as non empty Subset of (TOP-REAL 2) ;
A6: K1 c= NonZero (TOP-REAL 2)

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in K1 or z in NonZero (TOP-REAL 2) )
assume A7: z in K1 ; :: thesis: z in NonZero (TOP-REAL 2)
then ex p8 being Point of (TOP-REAL 2) st
( p8 = z & ( ( p8 `2 <= p8 `1 & - (p8 `1) <= p8 `2 ) or ( p8 `2 >= p8 `1 & p8 `2 <= - (p8 `1) ) ) & p8 <> 0. (TOP-REAL 2) ) by A2;
then not z in {(0. (TOP-REAL 2))} by TARSKI:def 1;
hence z in NonZero (TOP-REAL 2) by A7, XBOOLE_0:def 5; :: thesis: verum

end;

A8: dom (Out_In_Sq | K1) c= dom (proj2 * (Out_In_Sq | K1))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (Out_In_Sq | K1) or x in dom (proj2 * (Out_In_Sq | K1)) )
assume A9: x in dom (Out_In_Sq | K1) ; :: thesis: x in dom (proj2 * (Out_In_Sq | K1))
then x in (dom Out_In_Sq) /\ K1 by RELAT_1:61;
then x in dom Out_In_Sq by XBOOLE_0:def 4;
then Out_In_Sq . x in rng Out_In_Sq by FUNCT_1:3;
then A10: ( dom proj2 = the carrier of (TOP-REAL 2) & Out_In_Sq . x in the carrier of (TOP-REAL 2) ) by FUNCT_2:def 1, XBOOLE_0:def 5;
(Out_In_Sq | K1) . x = Out_In_Sq . x by A9, FUNCT_1:47;
hence x in dom (proj2 * (Out_In_Sq | K1)) by A9, A10, FUNCT_1:11; :: thesis: verum

end;

A11: rng (proj2 * (Out_In_Sq | K1)) c= the carrier of R^1 by TOPMETR:17;
A12: NonZero (TOP-REAL 2) <> {} by Th9;
A13: dom (Out_In_Sq | K1) c= dom (proj1 * (Out_In_Sq | K1))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (Out_In_Sq | K1) or x in dom (proj1 * (Out_In_Sq | K1)) )
assume A14: x in dom (Out_In_Sq | K1) ; :: thesis: x in dom (proj1 * (Out_In_Sq | K1))
then x in (dom Out_In_Sq) /\ K1 by RELAT_1:61;
then x in dom Out_In_Sq by XBOOLE_0:def 4;
then Out_In_Sq . x in rng Out_In_Sq by FUNCT_1:3;
then A15: ( dom proj1 = the carrier of (TOP-REAL 2) & Out_In_Sq . x in the carrier of (TOP-REAL 2) ) by FUNCT_2:def 1, XBOOLE_0:def 5;
(Out_In_Sq | K1) . x = Out_In_Sq . x by A14, FUNCT_1:47;
hence x in dom (proj1 * (Out_In_Sq | K1)) by A14, A15, FUNCT_1:11; :: thesis: verum

end;

A16: rng (proj1 * (Out_In_Sq | K1)) c= the carrier of R^1 by TOPMETR:17;
dom (proj1 * (Out_In_Sq | K1)) c= dom (Out_In_Sq | K1) by RELAT_1:25;
then dom (proj1 * (Out_In_Sq | K1)) = dom (Out_In_Sq | K1) by A13
.= (dom Out_In_Sq) /\ K1 by RELAT_1:61
.= (NonZero (TOP-REAL 2)) /\ K1 by A12, FUNCT_2:def 1
.= K1 by A6, XBOOLE_1:28
.= [#] ((TOP-REAL 2) | K1) by PRE_TOPC:def 5
.= the carrier of ((TOP-REAL 2) | K1) ;
then reconsider g1 = proj1 * (Out_In_Sq | K1) as Function of ((TOP-REAL 2) | K1),R^1 by A16, FUNCT_2:2;
for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds
g1 . p = 1 / (p `1)

proof

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

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in K1 or z in NonZero (TOP-REAL 2) )
assume A18: z in K1 ; :: thesis: z in NonZero (TOP-REAL 2)
then ex p8 being Point of (TOP-REAL 2) st
( p8 = z & ( ( p8 `2 <= p8 `1 & - (p8 `1) <= p8 `2 ) or ( p8 `2 >= p8 `1 & p8 `2 <= - (p8 `1) ) ) & p8 <> 0. (TOP-REAL 2) ) by A2;
then not z in {(0. (TOP-REAL 2))} by TARSKI:def 1;
hence z in NonZero (TOP-REAL 2) by A18, XBOOLE_0:def 5; :: thesis: verum

end;

A19: NonZero (TOP-REAL 2) <> {} by Th9;
A20: dom (Out_In_Sq | K1) = (dom Out_In_Sq) /\ K1 by RELAT_1:61
.= (NonZero (TOP-REAL 2)) /\ K1 by A19, FUNCT_2:def 1
.= K1 by A17, XBOOLE_1:28 ;
let p be Point of (TOP-REAL 2); :: thesis: ( p in the carrier of ((TOP-REAL 2) | K1) implies g1 . p = 1 / (p `1) )
A21: the carrier of ((TOP-REAL 2) | K1) = [#] ((TOP-REAL 2) | K1)
.= K1 by PRE_TOPC:def 5 ;
assume A22: p in the carrier of ((TOP-REAL 2) | K1) ; :: thesis: g1 . p = 1 / (p `1)
then ex p3 being Point of (TOP-REAL 2) st
( p = p3 & ( ( p3 `2 <= p3 `1 & - (p3 `1) <= p3 `2 ) or ( p3 `2 >= p3 `1 & p3 `2 <= - (p3 `1) ) ) & p3 <> 0. (TOP-REAL 2) ) by A2, A21;
then A23: Out_In_Sq . p = |[(1 / (p `1)),(((p `2) / (p `1)) / (p `1))]| by Def1;
(Out_In_Sq | K1) . p = Out_In_Sq . p by A22, A21, FUNCT_1:49;
then g1 . p = proj1 . |[(1 / (p `1)),(((p `2) / (p `1)) / (p `1))]| by A22, A20, A21, A23, FUNCT_1:13
.= |[(1 / (p `1)),(((p `2) / (p `1)) / (p `1))]| `1 by PSCOMP_1:def 5
.= 1 / (p `1) by EUCLID:52 ;
hence g1 . p = 1 / (p `1) ; :: thesis: verum

end;

then consider f1 being Function of ((TOP-REAL 2) | K1),R^1 such that
A24: for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds
f1 . p = 1 / (p `1) ;
dom (proj2 * (Out_In_Sq | K1)) c= dom (Out_In_Sq | K1) by RELAT_1:25;
then dom (proj2 * (Out_In_Sq | K1)) = dom (Out_In_Sq | K1) by A8
.= (dom Out_In_Sq) /\ K1 by RELAT_1:61
.= (NonZero (TOP-REAL 2)) /\ K1 by A12, FUNCT_2:def 1
.= K1 by A6, XBOOLE_1:28
.= [#] ((TOP-REAL 2) | K1) by PRE_TOPC:def 5
.= the carrier of ((TOP-REAL 2) | K1) ;
then reconsider g2 = proj2 * (Out_In_Sq | K1) as Function of ((TOP-REAL 2) | K1),R^1 by A11, 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 `2) / (p `1)) / (p `1)

proof

A25: NonZero (TOP-REAL 2) <> {} by Th9;
A26: dom (Out_In_Sq | K1) = (dom Out_In_Sq) /\ K1 by RELAT_1:61
.= (NonZero (TOP-REAL 2)) /\ K1 by A25, FUNCT_2:def 1
.= K1 by A6, XBOOLE_1:28 ;
let p be Point of (TOP-REAL 2); :: thesis: ( p in the carrier of ((TOP-REAL 2) | K1) implies g2 . p = ((p `2) / (p `1)) / (p `1) )
A27: the carrier of ((TOP-REAL 2) | K1) = [#] ((TOP-REAL 2) | K1)
.= K1 by PRE_TOPC:def 5 ;
assume A28: p in the carrier of ((TOP-REAL 2) | K1) ; :: thesis: g2 . p = ((p `2) / (p `1)) / (p `1)
then ex p3 being Point of (TOP-REAL 2) st
( p = p3 & ( ( p3 `2 <= p3 `1 & - (p3 `1) <= p3 `2 ) or ( p3 `2 >= p3 `1 & p3 `2 <= - (p3 `1) ) ) & p3 <> 0. (TOP-REAL 2) ) by A2, A27;
then A29: Out_In_Sq . p = |[(1 / (p `1)),(((p `2) / (p `1)) / (p `1))]| by Def1;
(Out_In_Sq | K1) . p = Out_In_Sq . p by A28, A27, FUNCT_1:49;
then g2 . p = proj2 . |[(1 / (p `1)),(((p `2) / (p `1)) / (p `1))]| by A28, A26, A27, A29, FUNCT_1:13
.= |[(1 / (p `1)),(((p `2) / (p `1)) / (p `1))]| `2 by PSCOMP_1:def 6
.= ((p `2) / (p `1)) / (p `1) by EUCLID:52 ;
hence g2 . p = ((p `2) / (p `1)) / (p `1) ; :: thesis: verum

end;

then consider f2 being Function of ((TOP-REAL 2) | K1),R^1 such that
A30: for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds
f2 . p = ((p `2) / (p `1)) / (p `1) ;
A31: for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K1) holds
q `1 <> 0

proof

let q be Point of (TOP-REAL 2); :: thesis: ( q in the carrier of ((TOP-REAL 2) | K1) implies q `1 <> 0 )
A32: the carrier of ((TOP-REAL 2) | K1) = [#] ((TOP-REAL 2) | K1)
.= K1 by PRE_TOPC:def 5 ;
assume q in the carrier of ((TOP-REAL 2) | K1) ; :: thesis: q `1 <> 0
then A33: ex p3 being Point of (TOP-REAL 2) st
( q = p3 & ( ( p3 `2 <= p3 `1 & - (p3 `1) <= p3 `2 ) or ( p3 `2 >= p3 `1 & p3 `2 <= - (p3 `1) ) ) & p3 <> 0. (TOP-REAL 2) ) by A2, A32;

now :: thesis: not q `1 = 0

assume A34: q `1 = 0 ; :: thesis: contradiction
then q `2 = 0 by A33;
hence contradiction by A33, A34, EUCLID:53, EUCLID:54; :: thesis: verum

end;

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

end;

then A35: f1 is continuous by A24, Th31;
A36: 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
A37: |[x,y]| in K1 and
A38: ( r = f1 . |[x,y]| & s = f2 . |[x,y]| ) ; :: thesis: f . |[x,y]| = |[r,s]|
set p99 = |[x,y]|;
A39: the carrier of ((TOP-REAL 2) | K1) = [#] ((TOP-REAL 2) | K1)
.= K1 by PRE_TOPC:def 5 ;
then A40: f1 . |[x,y]| = 1 / (|[x,y]| `1) by A24, A37;
A41: ex p3 being Point of (TOP-REAL 2) st
( |[x,y]| = p3 & ( ( p3 `2 <= p3 `1 & - (p3 `1) <= p3 `2 ) or ( p3 `2 >= p3 `1 & p3 `2 <= - (p3 `1) ) ) & p3 <> 0. (TOP-REAL 2) ) by A2, A37;
then ( ( ( |[x,y]| `2 <= |[x,y]| `1 & - (|[x,y]| `1) <= |[x,y]| `2 ) or ( |[x,y]| `2 >= |[x,y]| `1 & |[x,y]| `2 <= - (|[x,y]| `1) ) ) implies Out_In_Sq . |[x,y]| = |[(1 / (|[x,y]| `1)),(((|[x,y]| `2) / (|[x,y]| `1)) / (|[x,y]| `1))]| ) by Def1;
then (Out_In_Sq | K0) . |[x,y]| = |[(1 / (|[x,y]| `1)),(((|[x,y]| `2) / (|[x,y]| `1)) / (|[x,y]| `1))]| by A37, A41, FUNCT_1:49
.= |[r,s]| by A30, A37, A38, A39, A40 ;
hence f . |[x,y]| = |[r,s]| by A2; :: thesis: verum

end;

f2 is continuous by A31, A30, Th33;
hence f is continuous by A5, A3, A35, A36, Th35; :: thesis: verum