let A, B, C, D be category; :: thesis: ( A,B are_opposite & C,D are_opposite implies for F, G being covariant Functor of B,C st F,G are_naturally_equivalent holds
((dualizing-func (C,D)) * G) * (dualizing-func (A,B)),((dualizing-func (C,D)) * F) * (dualizing-func (A,B)) are_naturally_equivalent )
assume that
A1: A,B are_opposite and
A2: C,D are_opposite ; :: thesis: for F, G being covariant Functor of B,C st F,G are_naturally_equivalent holds
((dualizing-func (C,D)) * G) * (dualizing-func (A,B)),((dualizing-func (C,D)) * F) * (dualizing-func (A,B)) are_naturally_equivalent
let F, G be covariant Functor of B,C; :: thesis: ( F,G are_naturally_equivalent implies ((dualizing-func (C,D)) * G) * (dualizing-func (A,B)),((dualizing-func (C,D)) * F) * (dualizing-func (A,B)) are_naturally_equivalent )
assume that
A3: F is_naturally_transformable_to G and
A4: G is_transformable_to F ; :: according to FUNCTOR3:def 4 :: thesis: ( for b₁ being natural_transformation of F,G holds
not for b₂ being Element of the carrier of B holds b₁ ! b₂ is iso or ((dualizing-func (C,D)) * G) * (dualizing-func (A,B)),((dualizing-func (C,D)) * F) * (dualizing-func (A,B)) are_naturally_equivalent )
given t being natural_transformation of F,G such that A5: for a being Object of B holds t ! a is iso ; :: thesis: ((dualizing-func (C,D)) * G) * (dualizing-func (A,B)),((dualizing-func (C,D)) * F) * (dualizing-func (A,B)) are_naturally_equivalent
set dAB = dualizing-func (A,B);
set dCD = dualizing-func (C,D);
set dF = ((dualizing-func (C,D)) * F) * (dualizing-func (A,B));
set dG = ((dualizing-func (C,D)) * G) * (dualizing-func (A,B));
A6: F is_transformable_to G by A3;

A7: now :: thesis: for a being Object of A holds
( (((dualizing-func (C,D)) * G) * (dualizing-func (A,B))) . a = (dualizing-func (C,D)) . (G . ((dualizing-func (A,B)) . a)) & (((dualizing-func (C,D)) * F) * (dualizing-func (A,B))) . a = (dualizing-func (C,D)) . (F . ((dualizing-func (A,B)) . a)) & (((dualizing-func (C,D)) * G) * (dualizing-func (A,B))) . a = G . ((dualizing-func (A,B)) . a) & (((dualizing-func (C,D)) * F) * (dualizing-func (A,B))) . a = F . ((dualizing-func (A,B)) . a) & <^((((dualizing-func (C,D)) * G) * (dualizing-func (A,B))) . a),((((dualizing-func (C,D)) * F) * (dualizing-func (A,B))) . a)^> = <^(F . ((dualizing-func (A,B)) . a)),(G . ((dualizing-func (A,B)) . a))^> )

let a be Object of A; :: thesis: ( (((dualizing-func (C,D)) * G) * (dualizing-func (A,B))) . a = (dualizing-func (C,D)) . (G . ((dualizing-func (A,B)) . a)) & (((dualizing-func (C,D)) * F) * (dualizing-func (A,B))) . a = (dualizing-func (C,D)) . (F . ((dualizing-func (A,B)) . a)) & (((dualizing-func (C,D)) * G) * (dualizing-func (A,B))) . a = G . ((dualizing-func (A,B)) . a) & (((dualizing-func (C,D)) * F) * (dualizing-func (A,B))) . a = F . ((dualizing-func (A,B)) . a) & <^((((dualizing-func (C,D)) * G) * (dualizing-func (A,B))) . a),((((dualizing-func (C,D)) * F) * (dualizing-func (A,B))) . a)^> = <^(F . ((dualizing-func (A,B)) . a)),(G . ((dualizing-func (A,B)) . a))^> )
A8: (((dualizing-func (C,D)) * G) * (dualizing-func (A,B))) . a = ((dualizing-func (C,D)) * G) . ((dualizing-func (A,B)) . a) by FUNCTOR0:33;
(((dualizing-func (C,D)) * F) * (dualizing-func (A,B))) . a = ((dualizing-func (C,D)) * F) . ((dualizing-func (A,B)) . a) by FUNCTOR0:33;
hence ( (((dualizing-func (C,D)) * G) * (dualizing-func (A,B))) . a = (dualizing-func (C,D)) . (G . ((dualizing-func (A,B)) . a)) & (((dualizing-func (C,D)) * F) * (dualizing-func (A,B))) . a = (dualizing-func (C,D)) . (F . ((dualizing-func (A,B)) . a)) ) by A8, FUNCTOR0:33; :: thesis: ( (((dualizing-func (C,D)) * G) * (dualizing-func (A,B))) . a = G . ((dualizing-func (A,B)) . a) & (((dualizing-func (C,D)) * F) * (dualizing-func (A,B))) . a = F . ((dualizing-func (A,B)) . a) & <^((((dualizing-func (C,D)) * G) * (dualizing-func (A,B))) . a),((((dualizing-func (C,D)) * F) * (dualizing-func (A,B))) . a)^> = <^(F . ((dualizing-func (A,B)) . a)),(G . ((dualizing-func (A,B)) . a))^> )
hence ( (((dualizing-func (C,D)) * G) * (dualizing-func (A,B))) . a = G . ((dualizing-func (A,B)) . a) & (((dualizing-func (C,D)) * F) * (dualizing-func (A,B))) . a = F . ((dualizing-func (A,B)) . a) ) by A2, Def5; :: thesis: <^((((dualizing-func (C,D)) * G) * (dualizing-func (A,B))) . a),((((dualizing-func (C,D)) * F) * (dualizing-func (A,B))) . a)^> = <^(F . ((dualizing-func (A,B)) . a)),(G . ((dualizing-func (A,B)) . a))^>
hence <^((((dualizing-func (C,D)) * G) * (dualizing-func (A,B))) . a),((((dualizing-func (C,D)) * F) * (dualizing-func (A,B))) . a)^> = <^(F . ((dualizing-func (A,B)) . a)),(G . ((dualizing-func (A,B)) . a))^> by A2, Th9; :: thesis: verum

end;

A9: ((dualizing-func (C,D)) * G) * (dualizing-func (A,B)) is_transformable_to ((dualizing-func (C,D)) * F) * (dualizing-func (A,B))

proof

let a be Object of A; :: according to FUNCTOR2:def 1 :: thesis: not <^((((dualizing-func (C,D)) * G) * (dualizing-func (A,B))) . a),((((dualizing-func (C,D)) * F) * (dualizing-func (A,B))) . a)^> = {}
<^((((dualizing-func (C,D)) * G) * (dualizing-func (A,B))) . a),((((dualizing-func (C,D)) * F) * (dualizing-func (A,B))) . a)^> = <^(F . ((dualizing-func (A,B)) . a)),(G . ((dualizing-func (A,B)) . a))^> by A7;
hence not <^((((dualizing-func (C,D)) * G) * (dualizing-func (A,B))) . a),((((dualizing-func (C,D)) * F) * (dualizing-func (A,B))) . a)^> = {} by A6; :: thesis: verum

end;

dom t = the carrier of B by PARTFUN1:def 2
.= the carrier of A by A1 ;
then reconsider dt = t as ManySortedSet of the carrier of A by PARTFUN1:def 2, RELAT_1:def 18;
dt is transformation of ((dualizing-func (C,D)) * G) * (dualizing-func (A,B)),((dualizing-func (C,D)) * F) * (dualizing-func (A,B))

proof

thus ((dualizing-func (C,D)) * G) * (dualizing-func (A,B)) is_transformable_to ((dualizing-func (C,D)) * F) * (dualizing-func (A,B)) by A9; :: according to FUNCTOR2:def 2 :: thesis: for b₁ being Element of the carrier of A holds dt . b₁ is Element of <^((((dualizing-func (C,D)) * G) * (dualizing-func (A,B))) . b₁),((((dualizing-func (C,D)) * F) * (dualizing-func (A,B))) . b₁)^>
let a be Object of A; :: thesis: dt . a is Element of <^((((dualizing-func (C,D)) * G) * (dualizing-func (A,B))) . a),((((dualizing-func (C,D)) * F) * (dualizing-func (A,B))) . a)^>
set b = (dualizing-func (A,B)) . a;
A10: (dualizing-func (A,B)) . a = a by A1, Def5;
t . ((dualizing-func (A,B)) . a) = t ! ((dualizing-func (A,B)) . a) by A6, FUNCTOR2:def 4;
hence dt . a is Element of <^((((dualizing-func (C,D)) * G) * (dualizing-func (A,B))) . a),((((dualizing-func (C,D)) * F) * (dualizing-func (A,B))) . a)^> by A7, A10; :: thesis: verum

end;

then reconsider dt = dt as transformation of ((dualizing-func (C,D)) * G) * (dualizing-func (A,B)),((dualizing-func (C,D)) * F) * (dualizing-func (A,B)) ;

A11: now :: thesis: for a, b being Object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds (dt ! b) * ((((dualizing-func (C,D)) * G) * (dualizing-func (A,B))) . f) = ((((dualizing-func (C,D)) * F) * (dualizing-func (A,B))) . f) * (dt ! a)

let a, b be Object of A; :: thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b holds (dt ! b) * ((((dualizing-func (C,D)) * G) * (dualizing-func (A,B))) . f) = ((((dualizing-func (C,D)) * F) * (dualizing-func (A,B))) . f) * (dt ! a) )
assume A12: <^a,b^> <> {} ; :: thesis: for f being Morphism of a,b holds (dt ! b) * ((((dualizing-func (C,D)) * G) * (dualizing-func (A,B))) . f) = ((((dualizing-func (C,D)) * F) * (dualizing-func (A,B))) . f) * (dt ! a)
let f be Morphism of a,b; :: thesis: (dt ! b) * ((((dualizing-func (C,D)) * G) * (dualizing-func (A,B))) . f) = ((((dualizing-func (C,D)) * F) * (dualizing-func (A,B))) . f) * (dt ! a)
set b9 = (dualizing-func (A,B)) . b;
set a9 = (dualizing-func (A,B)) . a;
set f9 = (dualizing-func (A,B)) . f;
A13: (dualizing-func (A,B)) . a = a by A1, Def5;
A14: (dualizing-func (A,B)) . b = b by A1, Def5;
then A15: <^((dualizing-func (A,B)) . b),((dualizing-func (A,B)) . a)^> = <^a,b^> by A1, A13, Th9;
A16: t ! ((dualizing-func (A,B)) . a) = t . a by A6, A13, FUNCTOR2:def 4;
A17: t ! ((dualizing-func (A,B)) . b) = t . b by A6, A14, FUNCTOR2:def 4;
A18: dt ! a = t . a by A9, FUNCTOR2:def 4;
A19: dt ! b = t . b by A9, FUNCTOR2:def 4;
A20: <^(F . ((dualizing-func (A,B)) . b)),(F . ((dualizing-func (A,B)) . a))^> <> {} by A12, A15, FUNCTOR0:def 18;
A21: <^(G . ((dualizing-func (A,B)) . b)),(G . ((dualizing-func (A,B)) . a))^> <> {} by A12, A15, FUNCTOR0:def 18;
A22: (((dualizing-func (C,D)) * F) * (dualizing-func (A,B))) . f = ((dualizing-func (C,D)) * F) . ((dualizing-func (A,B)) . f) by A12, FUNCTOR3:7;
A23: (((dualizing-func (C,D)) * G) * (dualizing-func (A,B))) . f = ((dualizing-func (C,D)) * G) . ((dualizing-func (A,B)) . f) by A12, FUNCTOR3:7;
A24: (((dualizing-func (C,D)) * F) * (dualizing-func (A,B))) . f = (dualizing-func (C,D)) . (F . ((dualizing-func (A,B)) . f)) by A12, A15, A22, FUNCTOR3:8;
A25: (((dualizing-func (C,D)) * G) * (dualizing-func (A,B))) . f = (dualizing-func (C,D)) . (G . ((dualizing-func (A,B)) . f)) by A12, A15, A23, FUNCTOR3:8;
A26: (((dualizing-func (C,D)) * F) * (dualizing-func (A,B))) . f = F . ((dualizing-func (A,B)) . f) by A2, A20, A24, Def5;
A27: (((dualizing-func (C,D)) * G) * (dualizing-func (A,B))) . f = G . ((dualizing-func (A,B)) . f) by A2, A21, A25, Def5;
A28: <^(F . ((dualizing-func (A,B)) . b)),(G . ((dualizing-func (A,B)) . b))^> <> {} by A6;
A29: <^(F . ((dualizing-func (A,B)) . a)),(G . ((dualizing-func (A,B)) . a))^> <> {} by A6;
A30: (((dualizing-func (C,D)) * G) * (dualizing-func (A,B))) . a = G . ((dualizing-func (A,B)) . a) by A7;
A31: (((dualizing-func (C,D)) * F) * (dualizing-func (A,B))) . a = F . ((dualizing-func (A,B)) . a) by A7;
A32: (((dualizing-func (C,D)) * G) * (dualizing-func (A,B))) . b = G . ((dualizing-func (A,B)) . b) by A7;
A33: (((dualizing-func (C,D)) * F) * (dualizing-func (A,B))) . b = F . ((dualizing-func (A,B)) . b) by A7;
hence (dt ! b) * ((((dualizing-func (C,D)) * G) * (dualizing-func (A,B))) . f) = (G . ((dualizing-func (A,B)) . f)) * (t ! ((dualizing-func (A,B)) . b)) by A2, A17, A19, A21, A27, A28, A30, A32, Th9
.= (t ! ((dualizing-func (A,B)) . a)) * (F . ((dualizing-func (A,B)) . f)) by A3, A12, A15, FUNCTOR2:def 7
.= ((((dualizing-func (C,D)) * F) * (dualizing-func (A,B))) . f) * (dt ! a) by A2, A16, A18, A20, A26, A29, A30, A31, A33, Th9 ;
:: thesis: verum

end;

thus ((dualizing-func (C,D)) * G) * (dualizing-func (A,B)) is_naturally_transformable_to ((dualizing-func (C,D)) * F) * (dualizing-func (A,B)) by A9, A11; :: according to FUNCTOR3:def 4 :: thesis: ( ((dualizing-func (C,D)) * F) * (dualizing-func (A,B)) is_transformable_to ((dualizing-func (C,D)) * G) * (dualizing-func (A,B)) & ex b₁ being natural_transformation of ((dualizing-func (C,D)) * G) * (dualizing-func (A,B)),((dualizing-func (C,D)) * F) * (dualizing-func (A,B)) st
for b₂ being Element of the carrier of A holds b₁ ! b₂ is iso )
then reconsider dt = dt as natural_transformation of ((dualizing-func (C,D)) * G) * (dualizing-func (A,B)),((dualizing-func (C,D)) * F) * (dualizing-func (A,B)) by A11, FUNCTOR2:def 7;
thus ((dualizing-func (C,D)) * F) * (dualizing-func (A,B)) is_transformable_to ((dualizing-func (C,D)) * G) * (dualizing-func (A,B)) :: thesis: ex b₁ being natural_transformation of ((dualizing-func (C,D)) * G) * (dualizing-func (A,B)),((dualizing-func (C,D)) * F) * (dualizing-func (A,B)) st
for b₂ being Element of the carrier of A holds b₁ ! b₂ is iso

proof

let a be Object of A; :: according to FUNCTOR2:def 1 :: thesis: not <^((((dualizing-func (C,D)) * F) * (dualizing-func (A,B))) . a),((((dualizing-func (C,D)) * G) * (dualizing-func (A,B))) . a)^> = {}
A34: (((dualizing-func (C,D)) * F) * (dualizing-func (A,B))) . a = F . ((dualizing-func (A,B)) . a) by A7;
(((dualizing-func (C,D)) * G) * (dualizing-func (A,B))) . a = G . ((dualizing-func (A,B)) . a) by A7;
then <^((((dualizing-func (C,D)) * F) * (dualizing-func (A,B))) . a),((((dualizing-func (C,D)) * G) * (dualizing-func (A,B))) . a)^> = <^(G . ((dualizing-func (A,B)) . a)),(F . ((dualizing-func (A,B)) . a))^> by A2, A34, Th9;
hence not <^((((dualizing-func (C,D)) * F) * (dualizing-func (A,B))) . a),((((dualizing-func (C,D)) * G) * (dualizing-func (A,B))) . a)^> = {} by A4; :: thesis: verum

end;

take dt ; :: thesis: for b₁ being Element of the carrier of A holds dt ! b₁ is iso
let a be Object of A; :: thesis: dt ! a is iso
A35: (((dualizing-func (C,D)) * G) * (dualizing-func (A,B))) . a = G . ((dualizing-func (A,B)) . a) by A7;
A36: (((dualizing-func (C,D)) * F) * (dualizing-func (A,B))) . a = F . ((dualizing-func (A,B)) . a) by A7;
A37: (dualizing-func (A,B)) . a = a by A1, Def5;
A38: dt ! a = t . a by A9, FUNCTOR2:def 4;
A39: t ! ((dualizing-func (A,B)) . a) = t . a by A6, A37, FUNCTOR2:def 4;
A40: t ! ((dualizing-func (A,B)) . a) is iso by A5;
A41: <^(F . ((dualizing-func (A,B)) . a)),(G . ((dualizing-func (A,B)) . a))^> <> {} by A6;
<^(G . ((dualizing-func (A,B)) . a)),(F . ((dualizing-func (A,B)) . a))^> <> {} by A4;
hence dt ! a is iso by A2, A35, A36, A38, A39, A40, A41, Th23; :: thesis: verum