let
a
,
b
,
k
,
l
,
n
be
Nat
;
:: thesis:
(
n
=
(
(
a
,
b
)
In_Power
(
k
+
l
)
)
.
(
k
+
1
)
&
l
>
0
implies
a
divides
n
)
assume
(
n
=
(
(
a
,
b
)
In_Power
(
k
+
l
)
)
.
(
k
+
1
)
&
l
>
0
) ;
:: thesis:
a
divides
n
then
consider
x
being
Nat
such that
A2
:
n
=
a
*
x
by
Th50
;
thus
a
divides
n
by
A2
;
:: thesis:
verum