let
R
be
Ring
;
:: thesis:
for
a
being
Element
of
R
holds 2
'*'
a
=
a
+
a
let
a
be
Element
of
R
;
:: thesis:
2
'*'
a
=
a
+
a
thus
2
'*'
a
=
(
1
+
1
)
'*'
a
.=
(
1
'*'
a
)
+
(
1
'*'
a
)
by
RING_3:62
.=
a
+
(
1
'*'
a
)
by
RING_3:60
.=
a
+
a
by
RING_3:60
;
:: thesis:
verum