set Y1 = |[(- 1),1]|;
let D be non empty Subset of (TOP-REAL 2); :: thesis: ( D ` = {(0. (TOP-REAL 2))} implies ex h being Function of ((TOP-REAL 2) | D),((TOP-REAL 2) | D) st
( h = Sq_Circ | D & h is continuous ) )
A1: the carrier of ((TOP-REAL 2) | D) = D by PRE_TOPC:8;
dom Sq_Circ = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
then A2: dom (Sq_Circ | D) = the carrier of (TOP-REAL 2) /\ D by RELAT_1:61
.= the carrier of ((TOP-REAL 2) | D) by A1, XBOOLE_1:28 ;
assume A3: D ` = {(0. (TOP-REAL 2))} ; :: thesis: ex h being Function of ((TOP-REAL 2) | D),((TOP-REAL 2) | D) st
( h = Sq_Circ | D & h is continuous )
then A4: D = {(0. (TOP-REAL 2))} `
.= NonZero (TOP-REAL 2) by SUBSET_1:def 4 ;
A5: { 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) ) } c= the carrier of ((TOP-REAL 2) | D)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { 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) ) } or x in the carrier of ((TOP-REAL 2) | D) )
assume x in { 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: x in the carrier of ((TOP-REAL 2) | D)
then A6: ex p being Point of (TOP-REAL 2) st
( x = p & ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) & p <> 0. (TOP-REAL 2) ) ;
now :: thesis: x in D
assume not x in D ; :: thesis: contradiction
then x in the carrier of (TOP-REAL 2) \ D by A6, XBOOLE_0:def 5;
then x in D ` by SUBSET_1:def 4;
hence contradiction by A3, A6, TARSKI:def 1; :: thesis: verum
end;
hence x in the carrier of ((TOP-REAL 2) | D) by PRE_TOPC:8; :: thesis: verum
end;
1.REAL 2 in { 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) ) } by Lm9, Lm10;
then reconsider 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) ) } as non empty Subset of ((TOP-REAL 2) | D) by A5;
A7: K0 = the carrier of (((TOP-REAL 2) | D) | K0) by PRE_TOPC:8;
A8: { 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) ) } c= the carrier of ((TOP-REAL 2) | D)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { 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) ) } or x in the carrier of ((TOP-REAL 2) | D) )
assume x in { 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: x in the carrier of ((TOP-REAL 2) | D)
then A9: ex p being Point of (TOP-REAL 2) st
( x = p & ( ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) ) & p <> 0. (TOP-REAL 2) ) ;
now :: thesis: x in D
assume not x in D ; :: thesis: contradiction
then x in the carrier of (TOP-REAL 2) \ D by A9, XBOOLE_0:def 5;
then x in D ` by SUBSET_1:def 4;
hence contradiction by A3, A9, TARSKI:def 1; :: thesis: verum
end;
hence x in the carrier of ((TOP-REAL 2) | D) by PRE_TOPC:8; :: thesis: verum
end;
( |[(- 1),1]| `1 = - 1 & |[(- 1),1]| `2 = 1 ) by EUCLID:52;
then |[(- 1),1]| in { 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) ) } by JGRAPH_2:3;
then reconsider K1 = { 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) ) } as non empty Subset of ((TOP-REAL 2) | D) by A8;
A10: K1 = the carrier of (((TOP-REAL 2) | D) | K1) by PRE_TOPC:8;
A11: D c= K0 \/ K1
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in D or x in K0 \/ K1 )
assume A12: x in D ; :: thesis: x in K0 \/ K1
then reconsider px = x as Point of (TOP-REAL 2) ;
not x in {(0. (TOP-REAL 2))} by A4, A12, XBOOLE_0:def 5;
then ( ( ( ( px `2 <= px `1 & - (px `1) <= px `2 ) or ( px `2 >= px `1 & px `2 <= - (px `1) ) ) & px <> 0. (TOP-REAL 2) ) or ( ( ( px `1 <= px `2 & - (px `2) <= px `1 ) or ( px `1 >= px `2 & px `1 <= - (px `2) ) ) & px <> 0. (TOP-REAL 2) ) ) by TARSKI:def 1, XREAL_1:26;
then ( x in K0 or x in K1 ) ;
hence x in K0 \/ K1 by XBOOLE_0:def 3; :: thesis: verum
end;
A13: the carrier of ((TOP-REAL 2) | D) = [#] ((TOP-REAL 2) | D)
.= NonZero (TOP-REAL 2) by A4, PRE_TOPC:def 5 ;
A14: the carrier of ((TOP-REAL 2) | D) = D by PRE_TOPC:8;
A15: rng (Sq_Circ | K0) c= the carrier of (((TOP-REAL 2) | D) | K0)
proof
reconsider K00 = K0 as Subset of (TOP-REAL 2) by A14, XBOOLE_1:1;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (Sq_Circ | K0) or y in the carrier of (((TOP-REAL 2) | D) | K0) )
A16: for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K00) holds
q `1 <> 0
proof
let q be Point of (TOP-REAL 2); :: thesis: ( q in the carrier of ((TOP-REAL 2) | K00) implies q `1 <> 0 )
A17: the carrier of ((TOP-REAL 2) | K00) = K0 by PRE_TOPC:8;
assume q in the carrier of ((TOP-REAL 2) | K00) ; :: thesis: q `1 <> 0
then A18: 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 A17;
hence q `1 <> 0 ; :: thesis: verum
end;
assume y in rng (Sq_Circ | K0) ; :: thesis: y in the carrier of (((TOP-REAL 2) | D) | K0)
then consider x being object such that
A20: x in dom (Sq_Circ | K0) and
A21: y = (Sq_Circ | K0) . x by FUNCT_1:def 3;
A22: x in (dom Sq_Circ) /\ K0 by A20, RELAT_1:61;
then A23: x in K0 by XBOOLE_0:def 4;
K0 c= the carrier of (TOP-REAL 2) by A14, XBOOLE_1:1;
then reconsider p = x as Point of (TOP-REAL 2) by A23;
K00 = the carrier of ((TOP-REAL 2) | K00) by PRE_TOPC:8;
then p in the carrier of ((TOP-REAL 2) | K00) by A22, XBOOLE_0:def 4;
then A24: p `1 <> 0 by A16;
A25: ex px being Point of (TOP-REAL 2) st
( x = px & ( ( px `2 <= px `1 & - (px `1) <= px `2 ) or ( px `2 >= px `1 & px `2 <= - (px `1) ) ) & px <> 0. (TOP-REAL 2) ) by A23;
then A26: Sq_Circ . p = |[((p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2))))]| by Def1;
A27: sqrt (1 + (((p `2) / (p `1)) ^2)) > 0 by Lm1, SQUARE_1:25;
then ( ( (p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2))) <= (p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2))) & (- (p `1)) / (sqrt (1 + (((p `2) / (p `1)) ^2))) <= (p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2))) ) or ( (p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2))) >= (p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2))) & (p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2))) <= (- (p `1)) / (sqrt (1 + (((p `2) / (p `1)) ^2))) ) ) by A25, XREAL_1:72;
then A28: ( ( (p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2))) <= (p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2))) & - ((p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2)))) <= (p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2))) ) or ( (p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2))) >= (p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2))) & (p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2))) <= - ((p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2)))) ) ) by XCMPLX_1:187;
set p9 = |[((p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2))))]|;
A29: ( |[((p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2))))]| `1 = (p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2))) & |[((p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2))))]| `2 = (p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2))) ) by EUCLID:52;
A30: |[((p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2))))]| `1 = (p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2))) by EUCLID:52;
A31: now :: thesis: not |[((p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2))))]| = 0. (TOP-REAL 2)
assume |[((p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2))))]| = 0. (TOP-REAL 2) ; :: thesis: contradiction
then 0 * (sqrt (1 + (((p `2) / (p `1)) ^2))) = ((p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2)))) * (sqrt (1 + (((p `2) / (p `1)) ^2))) by A30, EUCLID:52, EUCLID:54;
hence contradiction by A24, A27, XCMPLX_1:87; :: thesis: verum
end;
Sq_Circ . p = y by A21, A23, FUNCT_1:49;
then y in K0 by A31, A26, A28, A29;
then y in [#] (((TOP-REAL 2) | D) | K0) by PRE_TOPC:def 5;
hence y in the carrier of (((TOP-REAL 2) | D) | K0) ; :: thesis: verum
end;
A32: K0 c= the carrier of (TOP-REAL 2)
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in K0 or z in the carrier of (TOP-REAL 2) )
assume z in K0 ; :: thesis: z in the carrier of (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) ) ;
hence z in the carrier of (TOP-REAL 2) ; :: thesis: verum
end;
dom (Sq_Circ | K0) = (dom Sq_Circ) /\ K0 by RELAT_1:61
.= the carrier of (TOP-REAL 2) /\ K0 by FUNCT_2:def 1
.= K0 by A32, XBOOLE_1:28 ;
then reconsider f = Sq_Circ | K0 as Function of (((TOP-REAL 2) | D) | K0),((TOP-REAL 2) | D) by A7, A15, FUNCT_2:2, XBOOLE_1:1;
A33: K1 = [#] (((TOP-REAL 2) | D) | K1) by PRE_TOPC:def 5;
A34: K1 c= the carrier of (TOP-REAL 2)
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in K1 or z in the carrier of (TOP-REAL 2) )
assume z in K1 ; :: thesis: z in the carrier of (TOP-REAL 2)
then ex p8 being Point of (TOP-REAL 2) st
( p8 = z & ( ( p8 `1 <= p8 `2 & - (p8 `2) <= p8 `1 ) or ( p8 `1 >= p8 `2 & p8 `1 <= - (p8 `2) ) ) & p8 <> 0. (TOP-REAL 2) ) ;
hence z in the carrier of (TOP-REAL 2) ; :: thesis: verum
end;
A35: rng (Sq_Circ | K1) c= the carrier of (((TOP-REAL 2) | D) | K1)
proof
reconsider K10 = K1 as Subset of (TOP-REAL 2) by A34;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (Sq_Circ | K1) or y in the carrier of (((TOP-REAL 2) | D) | K1) )
A36: for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K10) holds
q `2 <> 0
proof
let q be Point of (TOP-REAL 2); :: thesis: ( q in the carrier of ((TOP-REAL 2) | K10) implies q `2 <> 0 )
A37: the carrier of ((TOP-REAL 2) | K10) = K1 by PRE_TOPC:8;
assume q in the carrier of ((TOP-REAL 2) | K10) ; :: thesis: q `2 <> 0
then A38: ex p3 being Point of (TOP-REAL 2) st
( 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 A37;
hence q `2 <> 0 ; :: thesis: verum
end;
assume y in rng (Sq_Circ | K1) ; :: thesis: y in the carrier of (((TOP-REAL 2) | D) | K1)
then consider x being object such that
A40: x in dom (Sq_Circ | K1) and
A41: y = (Sq_Circ | K1) . x by FUNCT_1:def 3;
A42: x in (dom Sq_Circ) /\ K1 by A40, RELAT_1:61;
then A43: x in K1 by XBOOLE_0:def 4;
then reconsider p = x as Point of (TOP-REAL 2) by A34;
K10 = the carrier of ((TOP-REAL 2) | K10) by PRE_TOPC:8;
then p in the carrier of ((TOP-REAL 2) | K10) by A42, XBOOLE_0:def 4;
then A44: p `2 <> 0 by A36;
set p9 = |[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]|;
A45: ( |[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]| `2 = (p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))) & |[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]| `1 = (p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2))) ) by EUCLID:52;
A46: 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 A43;
then A47: Sq_Circ . p = |[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]| by Th4;
A48: sqrt (1 + (((p `1) / (p `2)) ^2)) > 0 by Lm1, SQUARE_1:25;
then ( ( (p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2))) <= (p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))) & (- (p `2)) / (sqrt (1 + (((p `1) / (p `2)) ^2))) <= (p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2))) ) or ( (p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2))) >= (p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))) & (p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2))) <= (- (p `2)) / (sqrt (1 + (((p `1) / (p `2)) ^2))) ) ) by A46, XREAL_1:72;
then A49: ( ( (p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2))) <= (p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))) & - ((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2)))) <= (p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2))) ) or ( (p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2))) >= (p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))) & (p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2))) <= - ((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2)))) ) ) by XCMPLX_1:187;
A50: |[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]| `2 = (p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))) by EUCLID:52;
A51: now :: thesis: not |[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]| = 0. (TOP-REAL 2)
assume |[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]| = 0. (TOP-REAL 2) ; :: thesis: contradiction
then 0 * (sqrt (1 + (((p `1) / (p `2)) ^2))) = ((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2)))) * (sqrt (1 + (((p `1) / (p `2)) ^2))) by A50, EUCLID:52, EUCLID:54;
hence contradiction by A44, A48, XCMPLX_1:87; :: thesis: verum
end;
Sq_Circ . p = y by A41, A43, FUNCT_1:49;
then y in K1 by A51, A47, A49, A45;
hence y in the carrier of (((TOP-REAL 2) | D) | K1) by PRE_TOPC:8; :: thesis: verum
end;
dom (Sq_Circ | K1) = (dom Sq_Circ) /\ K1 by RELAT_1:61
.= the carrier of (TOP-REAL 2) /\ K1 by FUNCT_2:def 1
.= K1 by A34, XBOOLE_1:28 ;
then reconsider g = Sq_Circ | K1 as Function of (((TOP-REAL 2) | D) | K1),((TOP-REAL 2) | D) by A10, A35, FUNCT_2:2, XBOOLE_1:1;
A52: dom g = K1 by A10, FUNCT_2:def 1;
g = Sq_Circ | K1 ;
then A53: K1 is closed by A4, Th18;
A54: K0 = [#] (((TOP-REAL 2) | D) | K0) by PRE_TOPC:def 5;
A55: for x being object st x in ([#] (((TOP-REAL 2) | D) | K0)) /\ ([#] (((TOP-REAL 2) | D) | K1)) holds
f . x = g . x
proof
let x be object ; :: thesis: ( x in ([#] (((TOP-REAL 2) | D) | K0)) /\ ([#] (((TOP-REAL 2) | D) | K1)) implies f . x = g . x )
assume A56: x in ([#] (((TOP-REAL 2) | D) | K0)) /\ ([#] (((TOP-REAL 2) | D) | K1)) ; :: thesis: f . x = g . x
then x in K0 by A54, XBOOLE_0:def 4;
then f . x = Sq_Circ . x by FUNCT_1:49;
hence f . x = g . x by A33, A56, FUNCT_1:49; :: thesis: verum
end;
f = Sq_Circ | K0 ;
then A57: K0 is closed by A4, Th17;
A58: dom f = K0 by A7, FUNCT_2:def 1;
D = [#] ((TOP-REAL 2) | D) by PRE_TOPC:def 5;
then A59: ([#] (((TOP-REAL 2) | D) | K0)) \/ ([#] (((TOP-REAL 2) | D) | K1)) = [#] ((TOP-REAL 2) | D) by A54, A33, A11;
A60: ( f is continuous & g is continuous ) by A4, Th17, Th18;
then consider h being Function of ((TOP-REAL 2) | D),((TOP-REAL 2) | D) such that
A61: h = f +* g and
h is continuous by A54, A33, A59, A57, A53, A55, JGRAPH_2:1;
( K0 = [#] (((TOP-REAL 2) | D) | K0) & K1 = [#] (((TOP-REAL 2) | D) | K1) ) by PRE_TOPC:def 5;
then A62: f tolerates g by A55, A58, A52, PARTFUN1:def 4;
A63: for x being object st x in dom h holds
h . x = (Sq_Circ | D) . x
proof
let x be object ; :: thesis: ( x in dom h implies h . x = (Sq_Circ | D) . x )
assume A64: x in dom h ; :: thesis: h . x = (Sq_Circ | D) . x
then reconsider p = x as Point of (TOP-REAL 2) by A13, XBOOLE_0:def 5;
not x in {(0. (TOP-REAL 2))} by A13, A64, XBOOLE_0:def 5;
then A65: x <> 0. (TOP-REAL 2) by TARSKI:def 1;
x in the carrier of (TOP-REAL 2) \ (D `) by A3, A13, A64;
then A66: x in (D `) ` by SUBSET_1:def 4;
per cases ( x in K0 or not x in K0 ) ;
suppose A67: x in K0 ; :: thesis: h . x = (Sq_Circ | D) . x
A68: (Sq_Circ | D) . p = Sq_Circ . p by A66, FUNCT_1:49
.= f . p by A67, FUNCT_1:49 ;
h . p = (g +* f) . p by A61, A62, FUNCT_4:34
.= f . p by A58, A67, FUNCT_4:13 ;
hence h . x = (Sq_Circ | D) . x by A68; :: thesis: verum
end;
suppose not x in K0 ; :: thesis: h . x = (Sq_Circ | D) . x
then ( not ( p `2 <= p `1 & - (p `1) <= p `2 ) & not ( p `2 >= p `1 & p `2 <= - (p `1) ) ) by A65;
then ( ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) ) by XREAL_1:26;
then A69: x in K1 by A65;
(Sq_Circ | D) . p = Sq_Circ . p by A66, FUNCT_1:49
.= g . p by A69, FUNCT_1:49 ;
hence h . x = (Sq_Circ | D) . x by A61, A52, A69, FUNCT_4:13; :: thesis: verum
end;
end;
end;
dom h = the carrier of ((TOP-REAL 2) | D) by FUNCT_2:def 1;
then f +* g = Sq_Circ | D by A61, A2, A63;
hence ex h being Function of ((TOP-REAL 2) | D),((TOP-REAL 2) | D) st
( h = Sq_Circ | D & h is continuous ) by A54, A33, A59, A57, A60, A53, A55, JGRAPH_2:1; :: thesis: verum