let a, b be Real; :: thesis: ( (a ^2) + (b ^2) = 1 iff |[a,b]| in circle (0,0,1) )

hereby :: thesis: ( |[a,b]| in circle (0,0,1) implies (a ^2) + (b ^2) = 1 )

assume A1: (a ^2) + (b ^2) = 1 ; :: thesis: |[a,b]| in circle (0,0,1)
reconsider p = |[a,b]| as Point of (TOP-REAL 2) ;
|.(p - |[0,0]|).| = 1

proof

|.(p - |[0,0]|).| ^2 = |.|[(a - 0),(b - 0)]|.| ^2 by EUCLID:62
.= 1 by A1, TOPGEN_5:9 ;
hence |.(p - |[0,0]|).| = 1 by SQUARE_1:41; :: thesis: verum

end;

hence |[a,b]| in circle (0,0,1) ; :: thesis: verum

end;

assume A2: |[a,b]| in circle (0,0,1) ; :: thesis: (a ^2) + (b ^2) = 1
thus (a ^2) + (b ^2) = |.|[(a - 0),(b - 0)]|.| ^2 by TOPGEN_5:9
.= |.(|[a,b]| - |[0,0]|).| ^2 by EUCLID:62
.= 1 ^2 by A2, TOPREAL9:43
.= 1 ; :: thesis: verum