let
a
be
Real
;
:: thesis:
(
a
>=
0
implies 1
-Root
a
=
a
)
assume
A1
:
a
>=
0
;
:: thesis:
1
-Root
a
=
a
a
|^
1 =
(
a
GeoSeq
)
.
(
0
+
1
)
by
Def1
.=
(
(
a
GeoSeq
)
.
0
)
*
a
by
Th3
.= 1
*
a
by
Th3
.=
a
;
hence
1
-Root
a
=
a
by
A1
,
Th19
;
:: thesis:
verum