let
x
be
real-valued
FinSequence
;
:: thesis:
|.
x
.|
=
sqrt
|(
x
,
x
)|
|.
x
.|
=
sqrt
(
|.
x
.|
^2
)
by
EUCLID:9
,
SQUARE_1:22
.=
sqrt
|(
x
,
x
)|
by
Th4
;
hence
|.
x
.|
=
sqrt
|(
x
,
x
)|
;
:: thesis:
verum