let D be Subset of (TOP-REAL 2); for K0 being Subset of ((TOP-REAL 2) | D) st 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
rng (Out_In_Sq | K0) c= the carrier of (((TOP-REAL 2) | D) | K0)
let K0 be Subset of ((TOP-REAL 2) | D); ( 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 rng (Out_In_Sq | K0) c= the carrier of (((TOP-REAL 2) | D) | K0) )
A1: the carrier of ((TOP-REAL 2) | D) =
[#] ((TOP-REAL 2) | D)
.=
D
by PRE_TOPC:def 5
;
then reconsider K00 = K0 as Subset of (TOP-REAL 2) by XBOOLE_1:1;
assume A2:
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) ) }
; rng (Out_In_Sq | K0) c= the carrier of (((TOP-REAL 2) | D) | K0)
A3:
for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K00) holds
q `2 <> 0
let y be object ; TARSKI:def 3 ( not y in rng (Out_In_Sq | K0) or y in the carrier of (((TOP-REAL 2) | D) | K0) )
assume
y in rng (Out_In_Sq | K0)
; y in the carrier of (((TOP-REAL 2) | D) | K0)
then consider x being object such that
A7:
x in dom (Out_In_Sq | K0)
and
A8:
y = (Out_In_Sq | K0) . x
by FUNCT_1:def 3;
x in (dom Out_In_Sq) /\ K0
by A7, RELAT_1:61;
then A9:
x in K0
by XBOOLE_0:def 4;
K0 c= the carrier of (TOP-REAL 2)
by A1, XBOOLE_1:1;
then reconsider p = x as Point of (TOP-REAL 2) by A9;
A10:
Out_In_Sq . p = y
by A8, A9, FUNCT_1:49;
A11:
ex px being Point of (TOP-REAL 2) st
( x = px & ( ( px `1 <= px `2 & - (px `2) <= px `1 ) or ( px `1 >= px `2 & px `1 <= - (px `2) ) ) & px <> 0. (TOP-REAL 2) )
by A2, A9;
then A12:
Out_In_Sq . p = |[(((p `1) / (p `2)) / (p `2)),(1 / (p `2))]|
by Th14;
A13: K00 =
[#] ((TOP-REAL 2) | K00)
by PRE_TOPC:def 5
.=
the carrier of ((TOP-REAL 2) | K00)
;
set p9 = |[(((p `1) / (p `2)) / (p `2)),(1 / (p `2))]|;
A14:
|[(((p `1) / (p `2)) / (p `2)),(1 / (p `2))]| `2 = 1 / (p `2)
by EUCLID:52;
A16:
p `2 <> 0
by A9, A13, A3;
now ( ( p `2 >= 0 & y in K0 ) or ( p `2 < 0 & y in K0 ) )per cases
( p `2 >= 0 or p `2 < 0 )
;
case A17:
p `2 >= 0
;
y in K0then
( (
(p `1) / (p `2) <= (p `2) / (p `2) &
(- (1 * (p `2))) / (p `2) <= (p `1) / (p `2) ) or (
p `1 >= p `2 &
p `1 <= - (1 * (p `2)) ) )
by A11, XREAL_1:72;
then A18:
( (
(p `1) / (p `2) <= 1 &
((- 1) * (p `2)) / (p `2) <= (p `1) / (p `2) ) or (
p `1 >= p `2 &
p `1 <= - (1 * (p `2)) ) )
by A9, A13, A3, XCMPLX_1:60;
then
( (
(p `1) / (p `2) <= 1 &
- 1
<= (p `1) / (p `2) ) or (
(p `1) / (p `2) >= 1 &
(p `1) / (p `2) <= ((- 1) * (p `2)) / (p `2) ) )
by A16, A17, XCMPLX_1:89;
then
(- 1) / (p `2) <= ((p `1) / (p `2)) / (p `2)
by A17, XREAL_1:72;
then A19:
( (
((p `1) / (p `2)) / (p `2) <= 1
/ (p `2) &
- (1 / (p `2)) <= ((p `1) / (p `2)) / (p `2) ) or (
((p `1) / (p `2)) / (p `2) >= 1
/ (p `2) &
((p `1) / (p `2)) / (p `2) <= - (1 / (p `2)) ) )
by A16, A17, A18, XREAL_1:72;
(
|[(((p `1) / (p `2)) / (p `2)),(1 / (p `2))]| `2 = 1
/ (p `2) &
|[(((p `1) / (p `2)) / (p `2)),(1 / (p `2))]| `1 = ((p `1) / (p `2)) / (p `2) )
by EUCLID:52;
hence
y in K0
by A2, A10, A15, A12, A19;
verum end; case A20:
p `2 < 0
;
y in K0then
( (
p `1 <= p `2 &
- (1 * (p `2)) <= p `1 ) or (
(p `1) / (p `2) <= (p `2) / (p `2) &
(p `1) / (p `2) >= (- (1 * (p `2))) / (p `2) ) )
by A11, XREAL_1:73;
then A21:
( (
p `1 <= p `2 &
- (1 * (p `2)) <= p `1 ) or (
(p `1) / (p `2) <= 1 &
(p `1) / (p `2) >= ((- 1) * (p `2)) / (p `2) ) )
by A20, XCMPLX_1:60;
then
( (
(p `1) / (p `2) >= 1 &
((- 1) * (p `2)) / (p `2) >= (p `1) / (p `2) ) or (
(p `1) / (p `2) <= 1 &
(p `1) / (p `2) >= - 1 ) )
by A20, XCMPLX_1:89;
then
(- 1) / (p `2) >= ((p `1) / (p `2)) / (p `2)
by A20, XREAL_1:73;
then A22:
( (
((p `1) / (p `2)) / (p `2) <= 1
/ (p `2) &
- (1 / (p `2)) <= ((p `1) / (p `2)) / (p `2) ) or (
((p `1) / (p `2)) / (p `2) >= 1
/ (p `2) &
((p `1) / (p `2)) / (p `2) <= - (1 / (p `2)) ) )
by A20, A21, XREAL_1:73;
(
|[(((p `1) / (p `2)) / (p `2)),(1 / (p `2))]| `2 = 1
/ (p `2) &
|[(((p `1) / (p `2)) / (p `2)),(1 / (p `2))]| `1 = ((p `1) / (p `2)) / (p `2) )
by EUCLID:52;
hence
y in K0
by A2, A10, A15, A12, A22;
verum end; end; end;
then
y in [#] (((TOP-REAL 2) | D) | K0)
by PRE_TOPC:def 5;
hence
y in the carrier of (((TOP-REAL 2) | D) | K0)
; verum