A2: n in NAT by ORDINAL1:def 12;
|.((p (/) |.p.|) - (0. (TOP-REAL n))).| = |.(p (/) |.p.|).| by RLVECT_1:13
.= 1 by A1, Th53 ;
then p (/) |.p.| in Sphere ((0. (TOP-REAL n)),1) by TOPREAL9:9;
hence p (/) |.p.| is Point of (Tcircle ((0. (TOP-REAL n)),1)) by A2, TOPREALB:9; :: thesis: verum