let A, B, C, D be category; :: thesis: ( A,B are_opposite & C,D are_opposite & A,C are_equivalent implies B,D are_equivalent )
assume A1: ( A,B are_opposite & C,D are_opposite ) ; :: thesis: ( not A,C are_equivalent or B,D are_equivalent )
given F being covariant Functor of A,C, G being covariant Functor of C,A such that A2: G * F, id A are_naturally_equivalent and
A3: F * G, id C are_naturally_equivalent ; :: according to YELLOW18:def 2 :: thesis: B,D are_equivalent
take dF = ((dualizing-func C,D) * F) * (dualizing-func B,A); :: according to YELLOW18:def 2 :: thesis: ex G being covariant Functor of D,B st
( G * dF, id B are_naturally_equivalent & dF * G, id D are_naturally_equivalent )
take dG = ((dualizing-func A,B) * G) * (dualizing-func D,C); :: thesis: ( dG * dF, id B are_naturally_equivalent & dF * dG, id D are_naturally_equivalent )
A4: ( G * (id C) = FunctorStr(# the ObjectMap of G,the MorphMap of G #) & (dualizing-func A,B) * (id A) = dualizing-func A,B ) by FUNCTOR3:5;
A5: id C = (dualizing-func D,C) * (dualizing-func C,D) by A1, Th15;
A6: ((dualizing-func A,B) * (G * F)) * (dualizing-func B,A) = (((dualizing-func A,B) * G) * F) * (dualizing-func B,A) by FUNCTOR0:33
.= ((dualizing-func A,B) * G) * (F * (dualizing-func B,A)) by FUNCTOR0:33
.= ((dualizing-func A,B) * (G * (id C))) * (F * (dualizing-func B,A)) by A4, Th3
.= (((dualizing-func A,B) * G) * (id C)) * (F * (dualizing-func B,A)) by FUNCTOR0:33
.= (dG * (dualizing-func C,D)) * (F * (dualizing-func B,A)) by A5, FUNCTOR0:33
.= dG * ((dualizing-func C,D) * (F * (dualizing-func B,A))) by FUNCTOR0:33
.= dG * dF by FUNCTOR0:33 ;
((dualizing-func A,B) * (id A)) * (dualizing-func B,A) = id B by A1, A4, Th15;
hence dG * dF, id B are_naturally_equivalent by A1, A2, A6, Th25; :: thesis: dF * dG, id D are_naturally_equivalent
A7: ( F * (id A) = FunctorStr(# the ObjectMap of F,the MorphMap of F #) & (dualizing-func C,D) * (id C) = dualizing-func C,D ) by FUNCTOR3:5;
A8: id A = (dualizing-func B,A) * (dualizing-func A,B) by A1, Th15;
A9: ((dualizing-func C,D) * (F * G)) * (dualizing-func D,C) = (((dualizing-func C,D) * F) * G) * (dualizing-func D,C) by FUNCTOR0:33
.= ((dualizing-func C,D) * F) * (G * (dualizing-func D,C)) by FUNCTOR0:33
.= ((dualizing-func C,D) * (F * (id A))) * (G * (dualizing-func D,C)) by A7, Th3
.= (((dualizing-func C,D) * F) * (id A)) * (G * (dualizing-func D,C)) by FUNCTOR0:33
.= (dF * (dualizing-func A,B)) * (G * (dualizing-func D,C)) by A8, FUNCTOR0:33
.= dF * ((dualizing-func A,B) * (G * (dualizing-func D,C))) by FUNCTOR0:33
.= dF * dG by FUNCTOR0:33 ;
((dualizing-func C,D) * (id C)) * (dualizing-func D,C) = id D by A1, A7, Th15;
hence dF * dG, id D are_naturally_equivalent by A1, A3, A9, Th25; :: thesis: verum