let
n
be
Nat
;
:: thesis:
for
R
being non
trivial
Ring
holds
dl.
(
R
,
n
)
=
[
1,
n
]
let
R
be non
trivial
Ring
;
:: thesis:
dl.
(
R
,
n
)
=
[
1,
n
]
thus
dl.
(
R
,
n
) =
dl.
n
by
SCMRING3:def 1
.=
[
1,
n
]
;
:: thesis:
verum