let A, B be category; ( A,B are_opposite implies (dualizing-func (A,B)) * (dualizing-func (B,A)) = id B )
assume A1:
A,B are_opposite
; (dualizing-func (A,B)) * (dualizing-func (B,A)) = id B
now for a, b being Object of B st <^a,b^> <> {} holds
for f being Morphism of a,b holds ((dualizing-func (A,B)) * (dualizing-func (B,A))) . f = (id B) . flet a,
b be
Object of
B;
( <^a,b^> <> {} implies for f being Morphism of a,b holds ((dualizing-func (A,B)) * (dualizing-func (B,A))) . f = (id B) . f )assume A3:
<^a,b^> <> {}
;
for f being Morphism of a,b holds ((dualizing-func (A,B)) * (dualizing-func (B,A))) . f = (id B) . fthen A4:
<^((dualizing-func (B,A)) . b),((dualizing-func (B,A)) . a)^> <> {}
by FUNCTOR0:def 19;
let f be
Morphism of
a,
b;
((dualizing-func (A,B)) * (dualizing-func (B,A))) . f = (id B) . fthus ((dualizing-func (A,B)) * (dualizing-func (B,A))) . f =
(dualizing-func (A,B)) . ((dualizing-func (B,A)) . f)
by A3, FUNCTOR3:7
.=
(dualizing-func (B,A)) . f
by A1, A4, Def5
.=
f
by A1, A3, Def5
.=
(id B) . f
by A3, FUNCTOR0:31
;
verum end;
hence
(dualizing-func (A,B)) * (dualizing-func (B,A)) = id B
by A2, Th1; verum