let
a
,
b
,
m
be
Nat
;
:: thesis:
(
m
>
0
implies ex
k
being
Nat
st
(
(
a
,
b
)
In_Power
m
)
.
1
=
a
*
k
)
(
m
>
0
implies ex
k
being
Nat
st
(
(
a
,
b
)
In_Power
(
m
+
0
)
)
.
(
0
+
1
)
=
a
*
k
)
by
Th50
;
hence
(
m
>
0
implies ex
k
being
Nat
st
(
(
a
,
b
)
In_Power
m
)
.
1
=
a
*
k
) ;
:: thesis:
verum