let
n
be
Nat
;
:: thesis:
for
p
being
Point
of
(
TOP-REAL
n
)
holds
|.
p
.|
=
sqrt
|(
p
,
p
)|
let
p
be
Point
of
(
TOP-REAL
n
)
;
:: thesis:
|.
p
.|
=
sqrt
|(
p
,
p
)|
|.
p
.|
=
sqrt
(
|.
p
.|
^2
)
by
SQUARE_1:22
,
TOPRNS_1:25
.=
sqrt
|(
p
,
p
)|
by
Th34
;
hence
|.
p
.|
=
sqrt
|(
p
,
p
)|
;
:: thesis:
verum