let D be non empty Subset of (TOP-REAL 2); :: thesis: ( D ` = {(0.REAL 2)} implies ex h being Function of ((TOP-REAL 2) | D),((TOP-REAL 2) | D) st
( h = (Sq_Circ " ) | D & h is continuous ) )
assume A1: D ` = {(0.REAL 2)} ; :: thesis: ex h being Function of ((TOP-REAL 2) | D),((TOP-REAL 2) | D) st
( h = (Sq_Circ " ) | D & h is continuous )
set B0 = {(0.REAL 2)};
A2: D = {(0.REAL 2)} ` by A1
.= the carrier of (TOP-REAL 2) \ {(0.REAL 2)} by SUBSET_1:def 5 ;
A3: { 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.REAL 2 ) } c= the carrier of ((TOP-REAL 2) | D)
proof
let x be set ; :: 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.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.REAL 2 ) } ; :: thesis: x in the carrier of ((TOP-REAL 2) | D)
then consider p being Point of (TOP-REAL 2) such that
A4: ( x = p & ( ( p `2 <= p `1 & - (p `1 ) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1 ) ) ) & p <> 0.REAL 2 ) ;
now
assume not x in D ; :: thesis: contradiction
then x in the carrier of (TOP-REAL 2) \ D by A4, XBOOLE_0:def 5;
then x in D ` by SUBSET_1:def 5;
hence contradiction by A1, A4, TARSKI:def 1; :: thesis: verum
end;
hence x in the carrier of ((TOP-REAL 2) | D) by PRE_TOPC:29; :: 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.REAL 2 ) } by Lm7;
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.REAL 2 ) } as non empty Subset of ((TOP-REAL 2) | D) by A3;
A5: { 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.REAL 2 ) } c= the carrier of ((TOP-REAL 2) | D)
proof
let x be set ; :: 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.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.REAL 2 ) } ; :: thesis: x in the carrier of ((TOP-REAL 2) | D)
then consider p being Point of (TOP-REAL 2) such that
A6: ( x = p & ( ( p `1 <= p `2 & - (p `2 ) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2 ) ) ) & p <> 0.REAL 2 ) ;
now
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 5;
hence contradiction by A1, A6, TARSKI:def 1; :: thesis: verum
end;
hence x in the carrier of ((TOP-REAL 2) | D) by PRE_TOPC:29; :: thesis: verum
end;
set Y1 = |[(- 1),1]|;
( |[(- 1),1]| `1 = - 1 & |[(- 1),1]| `2 = 1 ) by EUCLID:56;
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.REAL 2 ) } by JGRAPH_2:11;
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.REAL 2 ) } as non empty Subset of ((TOP-REAL 2) | D) by A5;
A7: K0 c= the carrier of (TOP-REAL 2)
proof
let z be set ; :: 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 consider p8 being Point of (TOP-REAL 2) such that
A8: ( p8 = z & ( ( p8 `2 <= p8 `1 & - (p8 `1 ) <= p8 `2 ) or ( p8 `2 >= p8 `1 & p8 `2 <= - (p8 `1 ) ) ) & p8 <> 0.REAL 2 ) ;
thus z in the carrier of (TOP-REAL 2) by A8; :: thesis: verum
end;
A9: dom ((Sq_Circ " ) | K0) = (dom (Sq_Circ " )) /\ K0 by FUNCT_1:68
.= the carrier of (TOP-REAL 2) /\ K0 by Th39, FUNCT_2:def 1
.= K0 by A7, XBOOLE_1:28 ;
A10: K0 = the carrier of (((TOP-REAL 2) | D) | K0) by PRE_TOPC:29;
rng ((Sq_Circ " ) | K0) c= the carrier of (((TOP-REAL 2) | D) | K0)
proof
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ((Sq_Circ " ) | K0) or y in the carrier of (((TOP-REAL 2) | D) | K0) )
assume y in rng ((Sq_Circ " ) | K0) ; :: thesis: y in the carrier of (((TOP-REAL 2) | D) | K0)
then consider x being set such that
A11: ( x in dom ((Sq_Circ " ) | K0) & y = ((Sq_Circ " ) | K0) . x ) by FUNCT_1:def 5;
A12: x in (dom (Sq_Circ " )) /\ K0 by A11, FUNCT_1:68;
then A13: x in K0 by XBOOLE_0:def 4;
then reconsider p = x as Point of (TOP-REAL 2) by A7;
A14: (Sq_Circ " ) . p = y by A11, A13, FUNCT_1:72;
consider px being Point of (TOP-REAL 2) such that
A15: ( x = px & ( ( px `2 <= px `1 & - (px `1 ) <= px `2 ) or ( px `2 >= px `1 & px `2 <= - (px `1 ) ) ) & px <> 0.REAL 2 ) by A13;
reconsider K00 = K0 as Subset of (TOP-REAL 2) by A7;
K00 = the carrier of ((TOP-REAL 2) | K00) by PRE_TOPC:29;
then A16: p in the carrier of ((TOP-REAL 2) | K00) by A12, XBOOLE_0:def 4;
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 )
assume A17: q in the carrier of ((TOP-REAL 2) | K00) ; :: thesis: q `1 <> 0
the carrier of ((TOP-REAL 2) | K00) = K0 by PRE_TOPC:29;
then consider p3 being Point of (TOP-REAL 2) such that
A18: ( q = p3 & ( ( p3 `2 <= p3 `1 & - (p3 `1 ) <= p3 `2 ) or ( p3 `2 >= p3 `1 & p3 `2 <= - (p3 `1 ) ) ) & p3 <> 0.REAL 2 ) by A17;
hence q `1 <> 0 ; :: thesis: verum
end;
then A20: p `1 <> 0 by A16;
set p9 = |[((p `1 ) * (sqrt (1 + (((p `2 ) / (p `1 )) ^2 )))),((p `2 ) * (sqrt (1 + (((p `2 ) / (p `1 )) ^2 ))))]|;
A21: ( |[((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:56;
A22: sqrt (1 + (((p `2 ) / (p `1 )) ^2 )) > 0 by Lm1, SQUARE_1:93;
A23: now
assume |[((p `1 ) * (sqrt (1 + (((p `2 ) / (p `1 )) ^2 )))),((p `2 ) * (sqrt (1 + (((p `2 ) / (p `1 )) ^2 ))))]| = 0.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 A21, EUCLID:56, EUCLID:58;
hence contradiction by A20, A22, XCMPLX_1:90; :: thesis: verum
end;
A24: (Sq_Circ " ) . p = |[((p `1 ) * (sqrt (1 + (((p `2 ) / (p `1 )) ^2 )))),((p `2 ) * (sqrt (1 + (((p `2 ) / (p `1 )) ^2 ))))]| by A15, Th38;
( ( (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 A15, A22, XREAL_1:66;
then A25: ( ( (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 )))) ) ) ;
( |[((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:56;
then y in K0 by A14, A23, A24, A25;
hence y in the carrier of (((TOP-REAL 2) | D) | K0) by PRE_TOPC:29; :: thesis: verum
end;
then reconsider f = (Sq_Circ " ) | K0 as Function of (((TOP-REAL 2) | D) | K0),((TOP-REAL 2) | D) by A9, A10, FUNCT_2:4, XBOOLE_1:1;
A26: K1 c= the carrier of (TOP-REAL 2)
proof
let z be set ; :: 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 consider p8 being Point of (TOP-REAL 2) such that
A27: ( p8 = z & ( ( p8 `1 <= p8 `2 & - (p8 `2 ) <= p8 `1 ) or ( p8 `1 >= p8 `2 & p8 `1 <= - (p8 `2 ) ) ) & p8 <> 0.REAL 2 ) ;
thus z in the carrier of (TOP-REAL 2) by A27; :: thesis: verum
end;
A28: dom ((Sq_Circ " ) | K1) = (dom (Sq_Circ " )) /\ K1 by FUNCT_1:68
.= the carrier of (TOP-REAL 2) /\ K1 by Th39, FUNCT_2:def 1
.= K1 by A26, XBOOLE_1:28 ;
A29: K1 = the carrier of (((TOP-REAL 2) | D) | K1) by PRE_TOPC:29;
rng ((Sq_Circ " ) | K1) c= the carrier of (((TOP-REAL 2) | D) | K1)
proof
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ((Sq_Circ " ) | K1) or y in the carrier of (((TOP-REAL 2) | D) | K1) )
assume y in rng ((Sq_Circ " ) | K1) ; :: thesis: y in the carrier of (((TOP-REAL 2) | D) | K1)
then consider x being set such that
A30: ( x in dom ((Sq_Circ " ) | K1) & y = ((Sq_Circ " ) | K1) . x ) by FUNCT_1:def 5;
A31: x in (dom (Sq_Circ " )) /\ K1 by A30, FUNCT_1:68;
then A32: x in K1 by XBOOLE_0:def 4;
then reconsider p = x as Point of (TOP-REAL 2) by A26;
A33: (Sq_Circ " ) . p = y by A30, A32, FUNCT_1:72;
consider px being Point of (TOP-REAL 2) such that
A34: ( x = px & ( ( px `1 <= px `2 & - (px `2 ) <= px `1 ) or ( px `1 >= px `2 & px `1 <= - (px `2 ) ) ) & px <> 0.REAL 2 ) by A32;
reconsider K10 = K1 as Subset of (TOP-REAL 2) by A26;
K10 = the carrier of ((TOP-REAL 2) | K10) by PRE_TOPC:29;
then A35: p in the carrier of ((TOP-REAL 2) | K10) by A31, XBOOLE_0:def 4;
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 )
assume A36: q in the carrier of ((TOP-REAL 2) | K10) ; :: thesis: q `2 <> 0
the carrier of ((TOP-REAL 2) | K10) = K1 by PRE_TOPC:29;
then consider p3 being Point of (TOP-REAL 2) such that
A37: ( q = p3 & ( ( p3 `1 <= p3 `2 & - (p3 `2 ) <= p3 `1 ) or ( p3 `1 >= p3 `2 & p3 `1 <= - (p3 `2 ) ) ) & p3 <> 0.REAL 2 ) by A36;
hence q `2 <> 0 ; :: thesis: verum
end;
then A39: p `2 <> 0 by A35;
set p9 = |[((p `1 ) * (sqrt (1 + (((p `1 ) / (p `2 )) ^2 )))),((p `2 ) * (sqrt (1 + (((p `1 ) / (p `2 )) ^2 ))))]|;
A40: ( |[((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 ))) & |[((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:56;
A41: sqrt (1 + (((p `1 ) / (p `2 )) ^2 )) > 0 by Lm1, SQUARE_1:93;
A42: now
assume |[((p `1 ) * (sqrt (1 + (((p `1 ) / (p `2 )) ^2 )))),((p `2 ) * (sqrt (1 + (((p `1 ) / (p `2 )) ^2 ))))]| = 0.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 A40, EUCLID:56, EUCLID:58;
hence contradiction by A39, A41, XCMPLX_1:90; :: thesis: verum
end;
A43: (Sq_Circ " ) . p = |[((p `1 ) * (sqrt (1 + (((p `1 ) / (p `2 )) ^2 )))),((p `2 ) * (sqrt (1 + (((p `1 ) / (p `2 )) ^2 ))))]| by A34, Th40;
( ( (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 A34, A41, XREAL_1:66;
then A44: ( ( (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 )))) ) ) ;
( |[((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:56;
then y in K1 by A33, A42, A43, A44;
hence y in the carrier of (((TOP-REAL 2) | D) | K1) by PRE_TOPC:29; :: thesis: verum
end;
then reconsider g = (Sq_Circ " ) | K1 as Function of (((TOP-REAL 2) | D) | K1),((TOP-REAL 2) | D) by A28, A29, FUNCT_2:4, XBOOLE_1:1;
A45: K0 = [#] (((TOP-REAL 2) | D) | K0) by PRE_TOPC:def 10;
A46: K1 = [#] (((TOP-REAL 2) | D) | K1) by PRE_TOPC:def 10;
A47: D = [#] ((TOP-REAL 2) | D) by PRE_TOPC:def 10;
D c= K0 \/ K1
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in D or x in K0 \/ K1 )
assume A48: x in D ; :: thesis: x in K0 \/ K1
then A49: ( x in the carrier of (TOP-REAL 2) & not x in {(0.REAL 2)} ) by A2, XBOOLE_0:def 5;
reconsider px = x as Point of (TOP-REAL 2) by A48;
( ( ( ( px `2 <= px `1 & - (px `1 ) <= px `2 ) or ( px `2 >= px `1 & px `2 <= - (px `1 ) ) ) & px <> 0.REAL 2 ) or ( ( ( px `1 <= px `2 & - (px `2 ) <= px `1 ) or ( px `1 >= px `2 & px `1 <= - (px `2 ) ) ) & px <> 0.REAL 2 ) ) by A49, TARSKI:def 1, XREAL_1:28;
then ( x in K0 or x in K1 ) ;
hence x in K0 \/ K1 by XBOOLE_0:def 3; :: thesis: verum
end;
then A50: ([#] (((TOP-REAL 2) | D) | K0)) \/ ([#] (((TOP-REAL 2) | D) | K1)) = [#] ((TOP-REAL 2) | D) by A45, A46, A47, XBOOLE_0:def 10;
( f = (Sq_Circ " ) | K0 & D = the carrier of (TOP-REAL 2) \ {(0.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.REAL 2 ) } ) by A2;
then A51: ( f is continuous & K0 is closed ) by Th49;
( g = (Sq_Circ " ) | K1 & D = the carrier of (TOP-REAL 2) \ {(0.REAL 2)} & 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.REAL 2 ) } ) by A2;
then A52: ( g is continuous & K1 is closed ) by Th50;
A53: now
let x be set ; :: thesis: ( x in ([#] (((TOP-REAL 2) | D) | K0)) /\ ([#] (((TOP-REAL 2) | D) | K1)) implies f . x = g . x )
assume A54: x in ([#] (((TOP-REAL 2) | D) | K0)) /\ ([#] (((TOP-REAL 2) | D) | K1)) ; :: thesis: f . x = g . x
then ( x in K0 & x in K1 ) by A45, A46, XBOOLE_0:def 4;
then f . x = (Sq_Circ " ) . x by FUNCT_1:72;
hence f . x = g . x by A46, A54, FUNCT_1:72; :: thesis: verum
end;
then consider h being Function of ((TOP-REAL 2) | D),((TOP-REAL 2) | D) such that
A55: ( h = f +* g & h is continuous ) by A45, A46, A50, A51, A52, JGRAPH_2:9;
A56: dom h = the carrier of ((TOP-REAL 2) | D) by FUNCT_2:def 1;
A57: the carrier of ((TOP-REAL 2) | D) = D by PRE_TOPC:29;
A58: the carrier of ((TOP-REAL 2) | D) = [#] ((TOP-REAL 2) | D)
.= the carrier of (TOP-REAL 2) \ {(0.REAL 2)} by A2, PRE_TOPC:def 10 ;
dom (Sq_Circ " ) = the carrier of (TOP-REAL 2) by Th39, FUNCT_2:def 1;
then A59: dom ((Sq_Circ " ) | D) = the carrier of (TOP-REAL 2) /\ D by FUNCT_1:68
.= the carrier of ((TOP-REAL 2) | D) by A57, XBOOLE_1:28 ;
A60: dom f = K0 by A10, FUNCT_2:def 1;
A61: K0 = [#] (((TOP-REAL 2) | D) | K0) by PRE_TOPC:def 10;
A62: dom g = K1 by A29, FUNCT_2:def 1;
K1 = [#] (((TOP-REAL 2) | D) | K1) by PRE_TOPC:def 10;
then A63: f tolerates g by A53, A60, A61, A62, PARTFUN1:def 6;
for x being set st x in dom h holds
h . x = ((Sq_Circ " ) | D) . x
proof
let x be set ; :: 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 ( x in the carrier of (TOP-REAL 2) & not x in {(0.REAL 2)} ) by A58, XBOOLE_0:def 5;
then A65: x <> 0.REAL 2 by TARSKI:def 1;
reconsider p = x as Point of (TOP-REAL 2) by A58, A64, XBOOLE_0:def 5;
x in the carrier of (TOP-REAL 2) \ (D ` ) by A1, A58, A64;
then A66: x in (D ` ) ` by SUBSET_1:def 5;
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:72
.= f . p by A67, FUNCT_1:72 ;
h . p = (g +* f) . p by A55, A63, FUNCT_4:35
.= f . p by A60, A67, FUNCT_4:14 ;
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:28;
then A69: x in K1 by A65;
((Sq_Circ " ) | D) . p = (Sq_Circ " ) . p by A66, FUNCT_1:72
.= g . p by A69, FUNCT_1:72 ;
hence h . x = ((Sq_Circ " ) | D) . x by A55, A62, A69, FUNCT_4:14; :: thesis: verum
end;
end;
end;
then f +* g = (Sq_Circ " ) | D by A55, A56, A59, FUNCT_1:9;
hence ex h being Function of ((TOP-REAL 2) | D),((TOP-REAL 2) | D) st
( h = (Sq_Circ " ) | D & h is continuous ) by A45, A46, A50, A51, A52, A53, JGRAPH_2:9; :: thesis: verum