let
R
be
Ring
;
:: thesis:
for
a
being
Element
of
R
holds
a
|^
2
=
a
*
a
let
a
be
Element
of
R
;
:: thesis:
a
|^
2
=
a
*
a
a
|^
(
1
+
1
)
=
(
a
|^
1
)
*
(
a
|^
1
)
by
BINOM:10
.=
a
*
(
a
|^
1
)
by
BINOM:8
.=
a
*
a
by
BINOM:8
;
hence
a
|^
2
=
a
*
a
;
:: thesis:
verum