let
C
be
Category
;
:: thesis:
for
f
being
Morphism
of
(
C
opp
)
holds
(
*id
C
)
.
f
=
opp
f
let
f
be
Morphism
of
(
C
opp
)
;
:: thesis:
(
*id
C
)
.
f
=
opp
f
thus
(
*id
C
)
.
f
=
(
id
C
)
.
(
opp
f
)
by
Def10
.=
opp
f
by
FUNCT_1:18
;
:: thesis:
verum