reconsider c1 = c[10] as Point of () ;
set aX2 = { q where q is Point of () : ( q in the carrier of & 0 >= q `2 ) } ;
set aX1 = { q where q is Point of () : ( q in the carrier of & 0 <= q `2 ) } ;
A1: { q where q is Point of () : ( q in the carrier of & 0 <= q `2 ) } c= the carrier of
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { q where q is Point of () : ( q in the carrier of & 0 <= q `2 ) } or x in the carrier of )
assume x in { q where q is Point of () : ( q in the carrier of & 0 <= q `2 ) } ; :: thesis: x in the carrier of
then ex q being Point of () st
( x = q & q in the carrier of & 0 <= q `2 ) ;
hence x in the carrier of ; :: thesis: verum
end;
A2: { q where q is Point of () : ( q in the carrier of & 0 >= q `2 ) } c= the carrier of
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { q where q is Point of () : ( q in the carrier of & 0 >= q `2 ) } or x in the carrier of )
assume x in { q where q is Point of () : ( q in the carrier of & 0 >= q `2 ) } ; :: thesis: x in the carrier of
then ex q being Point of () st
( x = q & q in the carrier of & 0 >= q `2 ) ;
hence x in the carrier of ; :: thesis: verum
end;
A3: Topen_unit_circle c[-10] is SubSpace of Topen_unit_circle c[-10] by TSEP_1:2;
A4: c1 `2 = 0 by EUCLID:52;
A5: c[10] is Point of by ;
then A6: c[10] in { q where q is Point of () : ( q in the carrier of & 0 <= q `2 ) } by A4;
A7: c[10] in { q where q is Point of () : ( q in the carrier of & 0 >= q `2 ) } by A4, A5;
then reconsider aX1 = { q where q is Point of () : ( q in the carrier of & 0 <= q `2 ) } , aX2 = { q where q is Point of () : ( q in the carrier of & 0 >= q `2 ) } as non empty Subset of by A1, A2, A6;
set X1 = | aX1;
let p be Point of ; :: thesis: ( p = c[10] implies Circle2IntervalL is_continuous_at p )
assume A8: p = c[10] ; :: thesis:
reconsider x1 = p as Point of ( | aX1) by ;
set X2 = | aX2;
reconsider x2 = p as Point of ( | aX2) by ;
A9: the carrier of ( | aX2) = aX2 by PRE_TOPC:8;
the carrier of c= aX1 \/ aX2
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in the carrier of or a in aX1 \/ aX2 )
assume A10: a in the carrier of ; :: thesis: a in aX1 \/ aX2
then reconsider a = a as Point of () by Lm8;
( 0 >= a `2 or 0 <= a `2 ) ;
then ( a in aX1 or a in aX2 ) by A10;
hence a in aX1 \/ aX2 by XBOOLE_0:def 3; :: thesis: verum
end;
then A11: the carrier of = aX1 \/ aX2 ;
Circle2IntervalL | ( | aX2) is continuous by Lm60;
then A12: Circle2IntervalL | ( | aX2) is_continuous_at x2 ;
Circle2IntervalL | ( | aX1) is continuous by Lm59;
then A13: Circle2IntervalL | ( | aX1) is_continuous_at x1 ;
the carrier of ( | aX1) = aX1 by PRE_TOPC:8;
then Topen_unit_circle c[-10] = ( | aX1) union ( | aX2) by ;
hence Circle2IntervalL is_continuous_at p by ; :: thesis: verum