let r be Real; :: thesis: for s being Point of (TOP-REAL 2) st s in Sphere ((0. (TOP-REAL 2)),r) holds
((s `1) ^2) + ((s `2) ^2) = r ^2
let s be Point of (TOP-REAL 2); :: thesis: ( s in Sphere ((0. (TOP-REAL 2)),r) implies ((s `1) ^2) + ((s `2) ^2) = r ^2 )
assume s in Sphere ((0. (TOP-REAL 2)),r) ; :: thesis: ((s `1) ^2) + ((s `2) ^2) = r ^2
then |.(s - (0. (TOP-REAL 2))).| = r by Th7;
then |.s.| = r by RLVECT_1:13;
hence ((s `1) ^2) + ((s `2) ^2) = r ^2 by JGRAPH_1:29; :: thesis: verum