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

let Kb, Cb be Subset of (); :: thesis: ( r >= 0 & Kb = { q where q is Point of () : |.q.| = 1 } & Cb = { p2 where p2 is Point of () : |.(p2 - |[a,b]|).| = r } implies (AffineMap (r,a,r,b)) .: Kb = Cb )
assume A1: ( r >= 0 & Kb = { q where q is Point of () : |.q.| = 1 } & Cb = { p2 where p2 is Point of () : |.(p2 - |[a,b]|).| = r } ) ; :: thesis: (AffineMap (r,a,r,b)) .: Kb = Cb
reconsider rr = r as Real ;
A2: (AffineMap (r,a,r,b)) .: Kb c= Cb
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (AffineMap (r,a,r,b)) .: Kb or y in Cb )
assume y in (AffineMap (r,a,r,b)) .: Kb ; :: thesis: y in Cb
then consider x being object such that
x in dom (AffineMap (r,a,r,b)) and
A3: x in Kb and
A4: y = (AffineMap (r,a,r,b)) . x by FUNCT_1:def 6;
consider p being Point of () such that
A5: x = p and
A6: |.p.| = 1 by A1, A3;
A7: (AffineMap (r,a,r,b)) . p = |[((r * (p `1)) + a),((r * (p `2)) + b)]| by JGRAPH_2:def 2;
then reconsider q = y as Point of () by A4, A5;
A8: q - |[a,b]| = |[(((r * (p `1)) + a) - a),(((r * (p `2)) + b) - b)]| by
.= r * |[(p `1),(p `2)]| by EUCLID:58
.= r * p by EUCLID:53 ;
|.(r * p).| = |.rr.| * |.p.| by TOPRNS_1:7
.= r by ;
hence y in Cb by A1, A8; :: thesis: verum
end;
Cb c= (AffineMap (r,a,r,b)) .: Kb
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Cb or y in (AffineMap (r,a,r,b)) .: Kb )
assume y in Cb ; :: thesis: y in (AffineMap (r,a,r,b)) .: Kb
then consider p2 being Point of () such that
A9: y = p2 and
A10: |.(p2 - |[a,b]|).| = r by A1;
now :: thesis: ( ( r > 0 & y in (AffineMap (r,a,r,b)) .: Kb ) or ( r = 0 & y in (AffineMap (r,a,r,b)) .: Kb ) )
per cases ( r > 0 or r = 0 ) by A1;
case A11: r > 0 ; :: thesis: y in (AffineMap (r,a,r,b)) .: Kb
set p1 = (1 / r) * (p2 - |[a,b]|);
|.((1 / r) * (p2 - |[a,b]|)).| = |.(1 / rr).| * |.(p2 - |[a,b]|).| by TOPRNS_1:7
.= (1 / r) * r by
.= 1 by ;
then A12: (1 / r) * (p2 - |[a,b]|) in Kb by A1;
A13: (1 / r) * (p2 - |[a,b]|) = |[((1 / r) * ((p2 - |[a,b]|) `1)),((1 / r) * ((p2 - |[a,b]|) `2))]| by EUCLID:57;
then A14: ((1 / r) * (p2 - |[a,b]|)) `1 = (1 / r) * ((p2 - |[a,b]|) `1) by EUCLID:52;
A15: ((1 / r) * (p2 - |[a,b]|)) `2 = (1 / r) * ((p2 - |[a,b]|) `2) by ;
A16: r * (((1 / r) * (p2 - |[a,b]|)) `1) = (r * (1 / r)) * ((p2 - |[a,b]|) `1) by A14
.= 1 * ((p2 - |[a,b]|) `1) by
.= (p2 `1) - (|[a,b]| `1) by TOPREAL3:3
.= (p2 `1) - a by EUCLID:52 ;
A17: r * (((1 / r) * (p2 - |[a,b]|)) `2) = (r * (1 / r)) * ((p2 - |[a,b]|) `2) by A15
.= 1 * ((p2 - |[a,b]|) `2) by
.= (p2 `2) - (|[a,b]| `2) by TOPREAL3:3
.= (p2 `2) - b by EUCLID:52 ;
A18: (AffineMap (r,a,r,b)) . ((1 / r) * (p2 - |[a,b]|)) = |[((r * (((1 / r) * (p2 - |[a,b]|)) `1)) + a),((r * (((1 / r) * (p2 - |[a,b]|)) `2)) + b)]| by JGRAPH_2:def 2
.= p2 by ;
dom (AffineMap (r,a,r,b)) = the carrier of () by FUNCT_2:def 1;
hence y in (AffineMap (r,a,r,b)) .: Kb by ; :: thesis: verum
end;
case A19: r = 0 ; :: thesis: y in (AffineMap (r,a,r,b)) .: Kb
set p1 = |[1,0]|;
A20: |[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 A21: |[1,0]| in Kb by A1;
A22: (AffineMap (r,a,r,b)) . |[1,0]| = |[((0 * (|[1,0]| `1)) + a),((0 * (|[1,0]| `2)) + b)]| by
.= p2 by ;
dom (AffineMap (r,a,r,b)) = the carrier of () by FUNCT_2:def 1;
hence y in (AffineMap (r,a,r,b)) .: Kb by ; :: thesis: verum
end;
end;
end;
hence y in (AffineMap (r,a,r,b)) .: Kb ; :: thesis: verum
end;
hence (AffineMap (r,a,r,b)) .: Kb = Cb by A2; :: thesis: verum