let
n
be
Nat
;
:: thesis:
(
n
>=
1 implies
n
-Root
1
=
1 )
A1
: 1
|^
n
=
1 ;
assume
n
>=
1 ;
:: thesis:
n
-Root
1
=
1
hence
n
-Root
1
=
1
by
A1
,
Def2
;
:: thesis:
verum