let
D
be non
empty
set
;
:: thesis:
for
p
being
Element
of
D
holds
Rotate
(
<*
p
*>
,
p
)
=
<*
p
*>
let
p
be
Element
of
D
;
:: thesis:
Rotate
(
<*
p
*>
,
p
)
=
<*
p
*>
<*
p
*>
/.
1
=
p
by
FINSEQ_4:16
;
hence
Rotate
(
<*
p
*>
,
p
)
=
<*
p
*>
by
Th89
;
:: thesis:
verum