let a, b, r be Real; :: thesis: for Cb being Subset of () st r > 0 & Cb = { p where p is Point of () : |.(p - |[a,b]|).| = r } holds
Cb is being_simple_closed_curve

let Cb be Subset of (); :: thesis: ( r > 0 & Cb = { p where p is Point of () : |.(p - |[a,b]|).| = r } implies Cb is being_simple_closed_curve )
assume that
A1: r > 0 and
A2: Cb = { p where p is Point of () : |.(p - |[a,b]|).| = r } ; :: thesis:
A3: |[r,0]| `1 = r by EUCLID:52;
A4: |[r,0]| `2 = 0 by EUCLID:52;
|.(|[(r + a),b]| - |[a,b]|).| = |.(|[(r + a),(0 + b)]| - |[a,b]|).|
.= |.((|[r,0]| + |[a,b]|) - |[a,b]|).| by EUCLID:56
.= |.(|[r,0]| + (|[a,b]| - |[a,b]|)).| by RLVECT_1:def 3
.= |.(|[r,0]| + (0. ())).| by RLVECT_1:5
.= by RLVECT_1:4
.= sqrt ((r ^2) + ()) by
.= r by ;
then |[(r + a),b]| in Cb by A2;
then reconsider Cbb = Cb as non empty Subset of () ;
set v = |[1,0]|;
A5: |[1,0]| `1 = 1 by EUCLID:52;
|[1,0]| `2 = 0 by EUCLID:52;
then = sqrt ((1 ^2) + ()) by
.= 1 by SQUARE_1:22 ;
then A6: |[1,0]| in { q where q is Point of () : |.q.| = 1 } ;
defpred S1[ Point of ()] means |.\$1.| = 1;
{ q where q is Element of () : S1[q] } is Subset of () from then reconsider Kb = { q where q is Point of () : |.q.| = 1 } as non empty Subset of () by A6;
A7: the carrier of (() | Kb) = Kb by PRE_TOPC:8;
set SC = AffineMap (r,a,r,b);
A8: AffineMap (r,a,r,b) is one-to-one by ;
A9: dom (AffineMap (r,a,r,b)) = the carrier of () by FUNCT_2:def 1;
A10: dom ((AffineMap (r,a,r,b)) | Kb) = (dom (AffineMap (r,a,r,b))) /\ Kb by RELAT_1:61
.= the carrier of (() | Kb) by ;
A11: rng ((AffineMap (r,a,r,b)) | Kb) c= ((AffineMap (r,a,r,b)) | Kb) .: the carrier of (() | Kb)
proof
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in rng ((AffineMap (r,a,r,b)) | Kb) or u in ((AffineMap (r,a,r,b)) | Kb) .: the carrier of (() | Kb) )
assume u in rng ((AffineMap (r,a,r,b)) | Kb) ; :: thesis: u in ((AffineMap (r,a,r,b)) | Kb) .: the carrier of (() | Kb)
then ex z being object st
( z in dom ((AffineMap (r,a,r,b)) | Kb) & u = ((AffineMap (r,a,r,b)) | Kb) . z ) by FUNCT_1:def 3;
hence u in ((AffineMap (r,a,r,b)) | Kb) .: the carrier of (() | Kb) by ; :: thesis: verum
end;
((AffineMap (r,a,r,b)) | Kb) .: the carrier of (() | Kb) = (AffineMap (r,a,r,b)) .: Kb by
.= Cb by A1, A2, Th20
.= the carrier of (() | Cbb) by PRE_TOPC:8 ;
then reconsider f0 = (AffineMap (r,a,r,b)) | Kb as Function of (() | Kb),(() | Cbb) by ;
rng ((AffineMap (r,a,r,b)) | Kb) c= the carrier of () ;
then reconsider f00 = f0 as Function of (() | Kb),() by ;
A12: rng f0 = ((AffineMap (r,a,r,b)) | Kb) .: the carrier of (() | Kb) by RELSET_1:22
.= (AffineMap (r,a,r,b)) .: Kb by
.= Cb by A1, A2, Th20 ;
A13: f0 is one-to-one by ;
Kb is compact by ;
then ex f1 being Function of (() | Kb),(() | Cbb) st
( f00 = f1 & f1 is being_homeomorphism ) by ;
hence Cb is being_simple_closed_curve by ; :: thesis: verum