let a, b be Real; ( (a ^2) + (b ^2) = 1 iff |[a,b]| in circle (0,0,1) )
assume A2:
|[a,b]| in circle (0,0,1)
; (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
; verum