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

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:34
.= (dualizing-func B,A) . a by A1, Def5
.= a by A1, Def5
.= (id B) . a by FUNCTOR0:30 ; :: thesis: verum

end;

now

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 20;
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:32 ; :: thesis: verum

end;

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