let
R
be
domRing
;
:: thesis:
for
a
being
Element
of
R
holds
LC
(
a

R
)
=
a
let
a
be
Element
of
R
;
:: thesis:
LC
(
a

R
)
=
a
thus
LC
(
a

R
)
=
LC
(
a
*
(
1_.
R
)
)
by
RING_4:16
.=
a
*
(
LC
(
1_.
R
)
)
by
prl0a
.=
a
*
(
1.
R
)
by
RATFUNC1:def 7
.=
a
;
:: thesis:
verum