let A, B be category; :: thesis: ( A,B are_opposite implies (dualizing-func (A,B)) * (dualizing-func (B,A)) = id B )
assume A1: A,B are_opposite ; :: thesis: (dualizing-func (A,B)) * (dualizing-func (B,A)) = id B

A2: now :: thesis: for a being Object of B holds ((dualizing-func (A,B)) * (dualizing-func (B,A))) . a = (id B) . a

let a be Object of B; :: thesis: ((dualizing-func (A,B)) * (dualizing-func (B,A))) . a = (id B) . a
thus ((dualizing-func (A,B)) * (dualizing-func (B,A))) . a = (dualizing-func (A,B)) . ((dualizing-func (B,A)) . a) by FUNCTOR0:33
.= (dualizing-func (B,A)) . a by A1, Def5
.= a by A1, Def5
.= (id B) . a by FUNCTOR0:29 ; :: thesis: verum

end;

now :: thesis: 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) . f

let a, b be Object of B; :: thesis: ( <^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^> <> {} ; :: thesis: for f being Morphism of a,b holds ((dualizing-func (A,B)) * (dualizing-func (B,A))) . f = (id B) . f
then A4: <^((dualizing-func (B,A)) . b),((dualizing-func (B,A)) . a)^> <> {} by FUNCTOR0:def 19;
let f be Morphism of a,b; :: thesis: ((dualizing-func (A,B)) * (dualizing-func (B,A))) . f = (id B) . f
thus ((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 ; :: thesis: verum

end;

hence (dualizing-func (A,B)) * (dualizing-func (B,A)) = id B by A2, Th1; :: thesis: verum