:: FUNCTOR3 semantic presentation

registration
cluster non empty transitive strict associative with_units AltCatStr ;
existence
ex b1 being non empty AltCatStr st
( b1 is transitive & b1 is associative & b1 is with_units & b1 is strict )
proof end;
end;

registration
let c1 be non empty transitive AltCatStr ;
let c2 be non empty with_units AltCatStr ;
cluster feasible strict Covariant Contravariant comp-preserving comp-reversing FunctorStr of a1,a2;
existence
ex b1 being FunctorStr of c1,c2 st
( b1 is strict & b1 is comp-preserving & b1 is comp-reversing & b1 is Covariant & b1 is Contravariant & b1 is feasible )
proof end;
end;

registration
let c1 be non empty transitive with_units AltCatStr ;
let c2 be non empty with_units AltCatStr ;
cluster feasible strict Covariant Contravariant id-preserving comp-preserving comp-reversing FunctorStr of a1,a2;
existence
ex b1 being FunctorStr of c1,c2 st
( b1 is strict & b1 is comp-preserving & b1 is comp-reversing & b1 is Covariant & b1 is Contravariant & b1 is feasible & b1 is id-preserving )
proof end;
end;

registration
let c1 be non empty transitive with_units AltCatStr ;
let c2 be non empty with_units AltCatStr ;
cluster feasible strict covariant contravariant Functor of a1,a2;
existence
ex b1 being Functor of c1,c2 st
( b1 is strict & b1 is feasible & b1 is covariant & b1 is contravariant )
proof end;
end;

theorem Th1: :: FUNCTOR3:1
for b1 being category
for b2, b3, b4, b5 being object of b1
for b6 being Morphism of b2,b3
for b7 being Morphism of b3,b4
for b8 being Morphism of b2,b5
for b9 being Morphism of b5,b4 st b7 * b6 = b9 * b8 & b6 * (b6 " ) = idm b3 & (b9 " ) * b9 = idm b5 & <^b2,b3^> <> {} & <^b3,b2^> <> {} & <^b3,b4^> <> {} & <^b4,b5^> <> {} & <^b5,b4^> <> {} holds
b8 * (b6 " ) = (b9 " ) * b7
proof end;

theorem Th2: :: FUNCTOR3:2
for b1 being non empty transitive AltCatStr
for b2, b3 being non empty with_units AltCatStr
for b4 being feasible Covariant FunctorStr of b1,b2
for b5 being FunctorStr of b2,b3
for b6, b7 being object of b1 holds Morph-Map (b5 * b4),b6,b7 = (Morph-Map b5,(b4 . b6),(b4 . b7)) * (Morph-Map b4,b6,b7)
proof end;

theorem Th3: :: FUNCTOR3:3
for b1 being non empty transitive AltCatStr
for b2, b3 being non empty with_units AltCatStr
for b4 being feasible Contravariant FunctorStr of b1,b2
for b5 being FunctorStr of b2,b3
for b6, b7 being object of b1 holds Morph-Map (b5 * b4),b6,b7 = (Morph-Map b5,(b4 . b7),(b4 . b6)) * (Morph-Map b4,b6,b7)
proof end;

Lemma1: for b1 being set
for b2 being non empty set
for b3 being Function of b1,b2
for b4 being ManySortedSet of b1
for b5 being ManySortedSet of b2 st ( for b6 being set st b6 in b1 & b4 . b6 <> {} holds
b5 . (b3 . b6) <> {} ) holds
for b6 being ManySortedFunction of b4,b5 * b3 holds ((id b5) * b3) ** b6 = b6
proof end;

theorem Th4: :: FUNCTOR3:4
for b1 being non empty transitive AltCatStr
for b2 being non empty with_units AltCatStr
for b3 being feasible FunctorStr of b1,b2 holds (id b2) * b3 = FunctorStr(# the ObjectMap of b3,the MorphMap of b3 #)
proof end;

theorem Th5: :: FUNCTOR3:5
for b1 being non empty transitive with_units AltCatStr
for b2 being non empty with_units AltCatStr
for b3 being feasible FunctorStr of b1,b2 holds b3 * (id b1) = FunctorStr(# the ObjectMap of b3,the MorphMap of b3 #)
proof end;

theorem Th6: :: FUNCTOR3:6
for b1 being non empty AltCatStr
for b2, b3 being non empty reflexive AltCatStr
for b4 being feasible Covariant FunctorStr of b1,b2
for b5 being feasible Covariant FunctorStr of b2,b3
for b6, b7 being object of b1
for b8 being Morphism of b6,b7 st <^b6,b7^> <> {} holds
(b5 * b4) . b8 = b5 . (b4 . b8)
proof end;

theorem Th7: :: FUNCTOR3:7
for b1 being non empty AltCatStr
for b2, b3 being non empty reflexive AltCatStr
for b4 being feasible Contravariant FunctorStr of b1,b2
for b5 being feasible Contravariant FunctorStr of b2,b3
for b6, b7 being object of b1
for b8 being Morphism of b6,b7 st <^b6,b7^> <> {} holds
(b5 * b4) . b8 = b5 . (b4 . b8)
proof end;

theorem Th8: :: FUNCTOR3:8
for b1 being non empty AltCatStr
for b2, b3 being non empty reflexive AltCatStr
for b4 being feasible Covariant FunctorStr of b1,b2
for b5 being feasible Contravariant FunctorStr of b2,b3
for b6, b7 being object of b1
for b8 being Morphism of b6,b7 st <^b6,b7^> <> {} holds
(b5 * b4) . b8 = b5 . (b4 . b8)
proof end;

theorem Th9: :: FUNCTOR3:9
for b1 being non empty AltCatStr
for b2, b3 being non empty reflexive AltCatStr
for b4 being feasible Covariant FunctorStr of b3,b2
for b5 being feasible Contravariant FunctorStr of b1,b3
for b6, b7 being object of b1
for b8 being Morphism of b6,b7 st <^b6,b7^> <> {} holds
(b4 * b5) . b8 = b4 . (b5 . b8)
proof end;

registration
let c1 be non empty transitive AltCatStr ;
let c2 be non empty transitive with_units AltCatStr ;
let c3 be non empty with_units AltCatStr ;
let c4 be feasible Covariant comp-preserving FunctorStr of c1,c2;
let c5 be feasible Covariant comp-preserving FunctorStr of c2,c3;
cluster a5 * a4 -> comp-preserving ;
coherence
c5 * c4 is comp-preserving
proof end;
end;

registration
let c1 be non empty transitive AltCatStr ;
let c2 be non empty transitive with_units AltCatStr ;
let c3 be non empty with_units AltCatStr ;
let c4 be feasible Contravariant comp-reversing FunctorStr of c1,c2;
let c5 be feasible Contravariant comp-reversing FunctorStr of c2,c3;
cluster a5 * a4 -> comp-preserving ;
coherence
c5 * c4 is comp-preserving
proof end;
end;

registration
let c1 be non empty transitive AltCatStr ;
let c2 be non empty transitive with_units AltCatStr ;
let c3 be non empty with_units AltCatStr ;
let c4 be feasible Covariant comp-preserving FunctorStr of c1,c2;
let c5 be feasible Contravariant comp-reversing FunctorStr of c2,c3;
cluster a5 * a4 -> comp-reversing ;
coherence
c5 * c4 is comp-reversing
proof end;
end;

registration
let c1 be non empty transitive AltCatStr ;
let c2 be non empty transitive with_units AltCatStr ;
let c3 be non empty with_units AltCatStr ;
let c4 be feasible Contravariant comp-reversing FunctorStr of c1,c2;
let c5 be feasible Covariant comp-preserving FunctorStr of c2,c3;
cluster a5 * a4 -> comp-reversing ;
coherence
c5 * c4 is comp-reversing
proof end;
end;

definition
let c1, c2 be non empty transitive with_units AltCatStr ;
let c3 be non empty with_units AltCatStr ;
let c4 be covariant Functor of c1,c2;
let c5 be covariant Functor of c2,c3;
redefine func * as c5 * c4 -> strict covariant Functor of a1,a3;
coherence
c5 * c4 is strict covariant Functor of c1,c3
proof end;
end;

definition
let c1, c2 be non empty transitive with_units AltCatStr ;
let c3 be non empty with_units AltCatStr ;
let c4 be contravariant Functor of c1,c2;
let c5 be contravariant Functor of c2,c3;
redefine func * as c5 * c4 -> strict covariant Functor of a1,a3;
coherence
c5 * c4 is strict covariant Functor of c1,c3
proof end;
end;

definition
let c1, c2 be non empty transitive with_units AltCatStr ;
let c3 be non empty with_units AltCatStr ;
let c4 be covariant Functor of c1,c2;
let c5 be contravariant Functor of c2,c3;
redefine func * as c5 * c4 -> strict contravariant Functor of a1,a3;
coherence
c5 * c4 is strict contravariant Functor of c1,c3
proof end;
end;

definition
let c1, c2 be non empty transitive with_units AltCatStr ;
let c3 be non empty with_units AltCatStr ;
let c4 be contravariant Functor of c1,c2;
let c5 be covariant Functor of c2,c3;
redefine func * as c5 * c4 -> strict contravariant Functor of a1,a3;
coherence
c5 * c4 is strict contravariant Functor of c1,c3
proof end;
end;

theorem Th10: :: FUNCTOR3:10
for b1, b2, b3 being non empty transitive with_units AltCatStr
for b4, b5 being covariant Functor of b1,b2
for b6, b7 being covariant Functor of b2,b3 st b4 is_transformable_to b5 & b6 is_transformable_to b7 holds
b6 * b4 is_transformable_to b7 * b5
proof end;

definition
let c1, c2, c3 be non empty transitive with_units AltCatStr ;
let c4, c5 be covariant Functor of c1,c2;
let c6 be transformation of c4,c5;
let c7 be covariant Functor of c2,c3;
assume E7: c4 is_transformable_to c5 ;
func c7 * c6 -> transformation of a7 * a4,a7 * a5 means :Def1: :: FUNCTOR3:def 1
for b1 being object of a1 holds a8 . b1 = a7 . (a6 ! b1);
existence
ex b1 being transformation of c7 * c4,c7 * c5 st
for b2 being object of c1 holds b1 . b2 = c7 . (c6 ! b2)
proof end;
uniqueness
for b1, b2 being transformation of c7 * c4,c7 * c5 st ( for b3 being object of c1 holds b1 . b3 = c7 . (c6 ! b3) ) & ( for b3 being object of c1 holds b2 . b3 = c7 . (c6 ! b3) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines * FUNCTOR3:def 1 :
for b1, b2, b3 being non empty transitive with_units AltCatStr
for b4, b5 being covariant Functor of b1,b2
for b6 being transformation of b4,b5
for b7 being covariant Functor of b2,b3 st b4 is_transformable_to b5 holds
for b8 being transformation of b7 * b4,b7 * b5 holds
( b8 = b7 * b6 iff for b9 being object of b1 holds b8 . b9 = b7 . (b6 ! b9) );

theorem Th11: :: FUNCTOR3:11
for b1, b2, b3 being non empty transitive with_units AltCatStr
for b4, b5 being covariant Functor of b3,b2
for b6 being covariant Functor of b2,b1
for b7 being transformation of b4,b5
for b8 being object of b3 st b4 is_transformable_to b5 holds
(b6 * b7) ! b8 = b6 . (b7 ! b8)
proof end;

definition
let c1, c2, c3 be non empty transitive with_units AltCatStr ;
let c4, c5 be covariant Functor of c2,c3;
let c6 be covariant Functor of c1,c2;
let c7 be transformation of c4,c5;
assume E9: c4 is_transformable_to c5 ;
func c7 * c6 -> transformation of a4 * a6,a5 * a6 means :Def2: :: FUNCTOR3:def 2
for b1 being object of a1 holds a8 . b1 = a7 ! (a6 . b1);
existence
ex b1 being transformation of c4 * c6,c5 * c6 st
for b2 being object of c1 holds b1 . b2 = c7 ! (c6 . b2)
proof end;
uniqueness
for b1, b2 being transformation of c4 * c6,c5 * c6 st ( for b3 being object of c1 holds b1 . b3 = c7 ! (c6 . b3) ) & ( for b3 being object of c1 holds b2 . b3 = c7 ! (c6 . b3) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines * FUNCTOR3:def 2 :
for b1, b2, b3 being non empty transitive with_units AltCatStr
for b4, b5 being covariant Functor of b2,b3
for b6 being covariant Functor of b1,b2
for b7 being transformation of b4,b5 st b4 is_transformable_to b5 holds
for b8 being transformation of b4 * b6,b5 * b6 holds
( b8 = b7 * b6 iff for b9 being object of b1 holds b8 . b9 = b7 ! (b6 . b9) );

theorem Th12: :: FUNCTOR3:12
for b1, b2, b3 being non empty transitive with_units AltCatStr
for b4 being covariant Functor of b3,b1
for b5, b6 being covariant Functor of b1,b2
for b7 being transformation of b5,b6
for b8 being object of b3 st b5 is_transformable_to b6 holds
(b7 * b4) ! b8 = b7 ! (b4 . b8)
proof end;

theorem Th13: :: FUNCTOR3:13
for b1, b2, b3 being non empty transitive with_units AltCatStr
for b4, b5, b6 being covariant Functor of b2,b3
for b7 being covariant Functor of b3,b1
for b8 being transformation of b4,b5
for b9 being transformation of b5,b6 st b4 is_transformable_to b5 & b5 is_transformable_to b6 holds
b7 * (b9 `*` b8) = (b7 * b9) `*` (b7 * b8)
proof end;

theorem Th14: :: FUNCTOR3:14
for b1, b2, b3 being non empty transitive with_units AltCatStr
for b4 being covariant Functor of b1,b2
for b5, b6, b7 being covariant Functor of b2,b3
for b8 being transformation of b5,b6
for b9 being transformation of b6,b7 st b5 is_transformable_to b6 & b6 is_transformable_to b7 holds
(b9 `*` b8) * b4 = (b9 * b4) `*` (b8 * b4)
proof end;

theorem Th15: :: FUNCTOR3:15
for b1, b2, b3, b4 being non empty transitive with_units AltCatStr
for b5 being covariant Functor of b1,b2
for b6 being covariant Functor of b2,b3
for b7, b8 being covariant Functor of b3,b4
for b9 being transformation of b7,b8 st b7 is_transformable_to b8 holds
(b9 * b6) * b5 = b9 * (b6 * b5)
proof end;

theorem Th16: :: FUNCTOR3:16
for b1, b2, b3, b4 being non empty transitive with_units AltCatStr
for b5 being covariant Functor of b1,b3
for b6, b7 being covariant Functor of b3,b4
for b8 being covariant Functor of b4,b2
for b9 being transformation of b6,b7 st b6 is_transformable_to b7 holds
(b8 * b9) * b5 = b8 * (b9 * b5)
proof end;

theorem Th17: :: FUNCTOR3:17
for b1, b2, b3, b4 being non empty transitive with_units AltCatStr
for b5, b6 being covariant Functor of b3,b4
for b7 being covariant Functor of b4,b1
for b8 being covariant Functor of b1,b2
for b9 being transformation of b5,b6 st b5 is_transformable_to b6 holds
(b8 * b7) * b9 = b8 * (b7 * b9)
proof end;

theorem Th18: :: FUNCTOR3:18
for b1, b2, b3 being non empty transitive with_units AltCatStr
for b4 being covariant Functor of b1,b2
for b5 being covariant Functor of b2,b3 holds (idt b5) * b4 = idt (b5 * b4)
proof end;

theorem Th19: :: FUNCTOR3:19
for b1, b2, b3 being non empty transitive with_units AltCatStr
for b4 being covariant Functor of b1,b2
for b5 being covariant Functor of b2,b3 holds b5 * (idt b4) = idt (b5 * b4)
proof end;

theorem Th20: :: FUNCTOR3:20
for b1, b2 being non empty transitive with_units AltCatStr
for b3, b4 being covariant Functor of b1,b2
for b5 being transformation of b3,b4 st b3 is_transformable_to b4 holds
(id b2) * b5 = b5
proof end;

theorem Th21: :: FUNCTOR3:21
for b1, b2 being non empty transitive with_units AltCatStr
for b3, b4 being covariant Functor of b2,b1
for b5 being transformation of b3,b4 st b3 is_transformable_to b4 holds
b5 * (id b2) = b5
proof end;

definition
let c1, c2, c3 be non empty transitive with_units AltCatStr ;
let c4, c5 be covariant Functor of c1,c2;
let c6, c7 be covariant Functor of c2,c3;
let c8 be transformation of c4,c5;
let c9 be transformation of c6,c7;
func c9 (#) c8 -> transformation of a6 * a4,a7 * a5 equals :: FUNCTOR3:def 3
(a9 * a5) `*` (a6 * a8);
coherence
(c9 * c5) `*` (c6 * c8) is transformation of c6 * c4,c7 * c5 ;
end;

:: deftheorem Def3 defines (#) FUNCTOR3:def 3 :
for b1, b2, b3 being non empty transitive with_units AltCatStr
for b4, b5 being covariant Functor of b1,b2
for b6, b7 being covariant Functor of b2,b3
for b8 being transformation of b4,b5
for b9 being transformation of b6,b7 holds b9 (#) b8 = (b9 * b5) `*` (b6 * b8);

theorem Th22: :: FUNCTOR3:22
for b1, b2, b3 being non empty transitive with_units AltCatStr
for b4, b5 being covariant Functor of b2,b3
for b6, b7 being covariant Functor of b3,b1
for b8 being transformation of b4,b5
for b9 being natural_transformation of b6,b7 st b4 is_transformable_to b5 & b6 is_naturally_transformable_to b7 holds
b9 (#) b8 = (b7 * b8) `*` (b9 * b4)
proof end;

theorem Th23: :: FUNCTOR3:23
for b1, b2 being non empty transitive with_units AltCatStr
for b3, b4 being covariant Functor of b1,b2
for b5 being transformation of b3,b4 st b3 is_transformable_to b4 holds
(idt (id b2)) (#) b5 = b5
proof end;

theorem Th24: :: FUNCTOR3:24
for b1, b2 being non empty transitive with_units AltCatStr
for b3, b4 being covariant Functor of b2,b1
for b5 being transformation of b3,b4 st b3 is_transformable_to b4 holds
b5 (#) (idt (id b2)) = b5
proof end;

theorem Th25: :: FUNCTOR3:25
for b1, b2, b3 being non empty transitive with_units AltCatStr
for b4, b5 being covariant Functor of b2,b3
for b6 being covariant Functor of b3,b1
for b7 being transformation of b4,b5 st b4 is_transformable_to b5 holds
b6 * b7 = (idt b6) (#) b7
proof end;

theorem Th26: :: FUNCTOR3:26
for b1, b2, b3 being non empty transitive with_units AltCatStr
for b4 being covariant Functor of b1,b2
for b5, b6 being covariant Functor of b2,b3
for b7 being transformation of b5,b6 st b5 is_transformable_to b6 holds
b7 * b4 = b7 (#) (idt b4)
proof end;

theorem Th27: :: FUNCTOR3:27
for b1, b2, b3, b4 being category
for b5, b6 being covariant Functor of b1,b2
for b7, b8 being covariant Functor of b2,b3
for b9, b10 being covariant Functor of b3,b4
for b11 being transformation of b5,b6
for b12 being transformation of b7,b8
for b13 being transformation of b9,b10 st b5 is_transformable_to b6 & b7 is_transformable_to b8 & b9 is_transformable_to b10 holds
(b13 (#) b12) (#) b11 = b13 (#) (b12 (#) b11)
proof end;

E21: now
let c1, c2, c3 be category;
let c4, c5 be covariant Functor of c1,c2;
let c6, c7 be covariant Functor of c2,c3;
let c8 be natural_transformation of c6,c7;
let c9 be natural_transformation of c4,c5;
assume E22: c4 is_naturally_transformable_to c5 ;
then E23: c4 is_transformable_to c5 by FUNCTOR2:def 6;
assume E24: c6 is_naturally_transformable_to c7 ;
then E25: c6 is_transformable_to c7 by FUNCTOR2:def 6;
set c10 = c8 (#) c9;
E26: now
let c11, c12 be object of c1;
assume E27: <^c11,c12^> <> {} ;
let c13 be Morphism of c11,c12;
E28: ( (c6 * c4) . c11 = c6 . (c4 . c11) & (c7 * c5) . c11 = c7 . (c5 . c11) ) by FUNCTOR0:34;
E29: ( (c6 * c4) . c12 = c6 . (c4 . c12) & (c7 * c5) . c12 = c7 . (c5 . c12) ) by FUNCTOR0:34;
E30: <^(c4 . c12),(c5 . c12)^> <> {} by E23, FUNCTOR2:def 1;
E31: <^(c4 . c11),(c4 . c12)^> <> {} by E27, FUNCTOR0:def 19;
then E32: <^(c4 . c11),(c5 . c12)^> <> {} by E30, ALTCAT_1:def 4;
E33: <^(c5 . c11),(c5 . c12)^> <> {} by E27, FUNCTOR0:def 19;
E34: <^(c4 . c11),(c5 . c11)^> <> {} by E23, FUNCTOR2:def 1;
E35: <^(c6 . (c4 . c11)),(c7 . (c4 . c11))^> <> {} by E25, FUNCTOR2:def 1;
E36: <^(c7 . (c4 . c11)),(c7 . (c5 . c11))^> <> {} by E34, FUNCTOR0:def 19;
E37: <^(c7 . (c5 . c11)),(c7 . (c5 . c12))^> <> {} by E33, FUNCTOR0:def 19;
E38: <^((c6 * c4) . c11),((c6 * c4) . c12)^> <> {} by E27, FUNCTOR0:def 19;
<^(c6 . (c4 . c12)),(c6 . (c5 . c12))^> <> {} by E30, FUNCTOR0:def 19;
then E39: <^((c6 * c4) . c12),((c6 * c5) . c12)^> <> {} by E29, FUNCTOR0:34;
<^(c6 . (c5 . c12)),(c7 . (c5 . c12))^> <> {} by E25, FUNCTOR2:def 1;
then E40: <^((c6 * c5) . c12),((c7 * c5) . c12)^> <> {} by E29, FUNCTOR0:34;
E41: c6 * c5 is_transformable_to c7 * c5 by E25, Th10;
E42: c6 * c4 is_transformable_to c6 * c5 by E23, Th10;
E43: c8 ! (c5 . c12) = (c8 * c5) . c12 by E25, Def2;
E44: c8 ! (c5 . c11) = (c8 * c5) . c11 by E25, Def2;
reconsider c14 = c6 . (c9 ! c12) as Morphism of ((c6 * c4) . c12),((c6 * c5) . c12) by E29, FUNCTOR0:34;
reconsider c15 = c8 ! (c5 . c12) as Morphism of ((c6 * c5) . c12),((c7 * c5) . c12) by E29, FUNCTOR0:34;
reconsider c16 = c6 . (c4 . c13) as Morphism of ((c6 * c4) . c11),((c6 * c4) . c12) by E29, FUNCTOR0:34;
reconsider c17 = c6 . ((c9 ! c12) * (c4 . c13)) as Morphism of ((c6 * c4) . c11),((c6 * c5) . c12) by E28, FUNCTOR0:34;
reconsider c18 = c6 . (c9 ! c11) as Morphism of ((c6 * c4) . c11),((c6 * c5) . c11) by E28, FUNCTOR0:34;
reconsider c19 = c8 ! (c5 . c11) as Morphism of ((c6 * c5) . c11),((c7 * c5) . c11) by E28, FUNCTOR0:34;
reconsider c20 = c7 . (c5 . c13) as Morphism of ((c7 * c5) . c11),((c7 * c5) . c12) by E28, FUNCTOR0:34;
E45: c6 . ((c9 ! c12) * (c4 . c13)) = (c6 . (c9 ! c12)) * (c6 . (c4 . c13)) by E30, E31, FUNCTOR0:def 24
.= c14 * c16 by E28, E29, FUNCTOR0:34 ;
thus ((c8 (#) c9) ! c12) * ((c6 * c4) . c13) = (((c8 * c5) ! c12) * ((c6 * c9) ! c12)) * ((c6 * c4) . c13) by E41, E42, FUNCTOR2:def 5
.= (c15 * ((c6 * c9) ! c12)) * ((c6 * c4) . c13) by E41, E43, FUNCTOR2:def 4
.= (c15 * c14) * ((c6 * c4) . c13) by E23, Th11
.= (c15 * c14) * c16 by E27, Th6
.= c15 * c17 by E38, E39, E40, E45, ALTCAT_1:25
.= (c8 ! (c5 . c12)) * (c6 . ((c9 ! c12) * (c4 . c13))) by E28, E29, FUNCTOR0:34
.= (c7 . ((c9 ! c12) * (c4 . c13))) * (c8 ! (c4 . c11)) by E24, E32, FUNCTOR2:def 7
.= (c7 . ((c5 . c13) * (c9 ! c11))) * (c8 ! (c4 . c11)) by E22, E27, FUNCTOR2:def 7
.= ((c7 . (c5 . c13)) * (c7 . (c9 ! c11))) * (c8 ! (c4 . c11)) by E33, E34, FUNCTOR0:def 24
.= (c7 . (c5 . c13)) * ((c7 . (c9 ! c11)) * (c8 ! (c4 . c11))) by E35, E36, E37, ALTCAT_1:25
.= (c7 . (c5 . c13)) * ((c8 ! (c5 . c11)) * (c6 . (c9 ! c11))) by E24, E34, FUNCTOR2:def 7
.= c20 * (c19 * c18) by E28, E29, FUNCTOR0:34
.= ((c7 * c5) . c13) * (c19 * c18) by E27, Th6
.= ((c7 * c5) . c13) * (((c8 * c5) ! c11) * c18) by E41, E44, FUNCTOR2:def 4
.= ((c7 * c5) . c13) * (((c8 * c5) ! c11) * ((c6 * c9) ! c11)) by E23, Th11
.= ((c7 * c5) . c13) * ((c8 (#) c9) ! c11) by E41, E42, FUNCTOR2:def 5 ;
end;
thus E27: c6 * c4 is_naturally_transformable_to c7 * c5
proof
thus c6 * c4 is_transformable_to c7 * c5 by E23, E25, Th10; :: according to FUNCTOR2:def 6
take c8 (#) c9 ;
thus for b1, b2 being M2(the carrier of c1) holds
( <^b1,b2^> = {} or for b3 being M2(<^b1,b2^>) holds ((c8 (#) c9) ! b2) * ((c6 * c4) . b3) = ((c7 * c5) . b3) * ((c8 (#) c9) ! b1) ) by E26;
end;
thus c8 (#) c9 is natural_transformation of c6 * c4,c7 * c5
proof
thus c6 * c4 is_naturally_transformable_to c7 * c5 by E27; :: according to FUNCTOR2:def 7
thus for b1, b2 being M2(the carrier of c1) holds
( <^b1,b2^> = {} or for b3 being M2(<^b1,b2^>) holds ((c8 (#) c9) ! b2) * ((c6 * c4) . b3) = ((c7 * c5) . b3) * ((c8 (#) c9) ! b1) ) by E26;
end;
end;

theorem Th28: :: FUNCTOR3:28
for b1, b2, b3 being category
for b4, b5 being covariant Functor of b2,b3
for b6 being covariant Functor of b3,b1
for b7 being natural_transformation of b4,b5 st b4 is_naturally_transformable_to b5 holds
b6 * b7 is natural_transformation of b6 * b4,b6 * b5
proof end;

theorem Th29: :: FUNCTOR3:29
for b1, b2, b3 being category
for b4 being covariant Functor of b1,b2
for b5, b6 being covariant Functor of b2,b3
for b7 being natural_transformation of b5,b6 st b5 is_naturally_transformable_to b6 holds
b7 * b4 is natural_transformation of b5 * b4,b6 * b4
proof end;

theorem Th30: :: FUNCTOR3:30
for b1, b2, b3 being category
for b4, b5 being covariant Functor of b1,b2
for b6, b7 being covariant Functor of b2,b3
for b8 being natural_transformation of b4,b5
for b9 being natural_transformation of b6,b7 st b4 is_naturally_transformable_to b5 & b6 is_naturally_transformable_to b7 holds
( b6 * b4 is_naturally_transformable_to b7 * b5 & b9 (#) b8 is natural_transformation of b6 * b4,b7 * b5 ) by Lemma21;

theorem Th31: :: FUNCTOR3:31
for b1, b2, b3 being category
for b4, b5, b6 being covariant Functor of b1,b2
for b7, b8, b9 being covariant Functor of b2,b3
for b10 being natural_transformation of b7,b8
for b11 being natural_transformation of b8,b9
for b12 being transformation of b4,b5
for b13 being transformation of b5,b6 st b4 is_naturally_transformable_to b5 & b5 is_naturally_transformable_to b6 & b7 is_naturally_transformable_to b8 & b8 is_naturally_transformable_to b9 holds
(b11 `*` b10) (#) (b13 `*` b12) = (b11 (#) b13) `*` (b10 (#) b12)
proof end;

theorem Th32: :: FUNCTOR3:32
for b1, b2 being category
for b3, b4 being covariant Functor of b2,b1
for b5 being natural_transformation of b3,b4 st b3 is_naturally_transformable_to b4 & b4 is_transformable_to b3 & ( for b6 being object of b2 holds b5 ! b6 is iso ) holds
( b4 is_naturally_transformable_to b3 & ex b6 being natural_transformation of b4,b3 st
for b7 being object of b2 holds
( b6 . b7 = (b5 ! b7) " & b6 ! b7 is iso ) )
proof end;

definition
let c1, c2 be category;
let c3, c4 be covariant Functor of c1,c2;
pred c3,c4 are_naturally_equivalent means :Def4: :: FUNCTOR3:def 4
( a3 is_naturally_transformable_to a4 & a4 is_transformable_to a3 & ex b1 being natural_transformation of a3,a4 st
for b2 being object of a1 holds b1 ! b2 is iso );
reflexivity
for b1 being covariant Functor of c1,c2 holds
( b1 is_naturally_transformable_to b1 & b1 is_transformable_to b1 & ex b2 being natural_transformation of b1,b1 st
for b3 being object of c1 holds b2 ! b3 is iso )
proof end;
symmetry
for b1, b2 being covariant Functor of c1,c2 st b1 is_naturally_transformable_to b2 & b2 is_transformable_to b1 & ex b3 being natural_transformation of b1,b2 st
for b4 being object of c1 holds b3 ! b4 is iso holds
( b2 is_naturally_transformable_to b1 & b1 is_transformable_to b2 & ex b3 being natural_transformation of b2,b1 st
for b4 being object of c1 holds b3 ! b4 is iso )
proof end;
end;

:: deftheorem Def4 defines are_naturally_equivalent FUNCTOR3:def 4 :
for b1, b2 being category
for b3, b4 being covariant Functor of b1,b2 holds
( b3,b4 are_naturally_equivalent iff ( b3 is_naturally_transformable_to b4 & b4 is_transformable_to b3 & ex b5 being natural_transformation of b3,b4 st
for b6 being object of b1 holds b5 ! b6 is iso ) );

definition
let c1, c2 be category;
let c3, c4 be covariant Functor of c1,c2;
assume E26: c3,c4 are_naturally_equivalent ;
mode natural_equivalence of c3,c4 -> natural_transformation of a3,a4 means :Def5: :: FUNCTOR3:def 5
for b1 being object of a1 holds a5 ! b1 is iso;
existence
ex b1 being natural_transformation of c3,c4 st
for b2 being object of c1 holds b1 ! b2 is iso by E26, Def4;
end;

:: deftheorem Def5 defines natural_equivalence FUNCTOR3:def 5 :
for b1, b2 being category
for b3, b4 being covariant Functor of b1,b2 st b3,b4 are_naturally_equivalent holds
for b5 being natural_transformation of b3,b4 holds
( b5 is natural_equivalence of b3,b4 iff for b6 being object of b1 holds b5 ! b6 is iso );

theorem Th33: :: FUNCTOR3:33
for b1, b2 being category
for b3, b4, b5 being covariant Functor of b1,b2 st b3,b4 are_naturally_equivalent & b4,b5 are_naturally_equivalent holds
b3,b5 are_naturally_equivalent
proof end;

theorem Th34: :: FUNCTOR3:34
for b1, b2 being category
for b3, b4, b5 being covariant Functor of b1,b2
for b6 being natural_equivalence of b3,b4
for b7 being natural_equivalence of b4,b5 st b3,b4 are_naturally_equivalent & b4,b5 are_naturally_equivalent holds
b7 `*` b6 is natural_equivalence of b3,b5
proof end;

theorem Th35: :: FUNCTOR3:35
for b1, b2, b3 being category
for b4, b5 being covariant Functor of b2,b3
for b6 being covariant Functor of b3,b1
for b7 being natural_equivalence of b4,b5 st b4,b5 are_naturally_equivalent holds
( b6 * b4,b6 * b5 are_naturally_equivalent & b6 * b7 is natural_equivalence of b6 * b4,b6 * b5 )
proof end;

theorem Th36: :: FUNCTOR3:36
for b1, b2, b3 being category
for b4 being covariant Functor of b1,b2
for b5, b6 being covariant Functor of b2,b3
for b7 being natural_equivalence of b5,b6 st b5,b6 are_naturally_equivalent holds
( b5 * b4,b6 * b4 are_naturally_equivalent & b7 * b4 is natural_equivalence of b5 * b4,b6 * b4 )
proof end;

theorem Th37: :: FUNCTOR3:37
for b1, b2, b3 being category
for b4, b5 being covariant Functor of b1,b2
for b6, b7 being covariant Functor of b2,b3
for b8 being natural_equivalence of b4,b5
for b9 being natural_equivalence of b6,b7 st b4,b5 are_naturally_equivalent & b6,b7 are_naturally_equivalent holds
( b6 * b4,b7 * b5 are_naturally_equivalent & b9 (#) b8 is natural_equivalence of b6 * b4,b7 * b5 )
proof end;

definition
let c1, c2 be category;
let c3, c4 be covariant Functor of c1,c2;
let c5 be natural_equivalence of c3,c4;
assume E31: c3,c4 are_naturally_equivalent ;
func c5 " -> natural_equivalence of a4,a3 means :Def6: :: FUNCTOR3:def 6
for b1 being object of a1 holds a6 . b1 = (a5 ! b1) " ;
existence
ex b1 being natural_equivalence of c4,c3 st
for b2 being object of c1 holds b1 . b2 = (c5 ! b2) "
proof end;
uniqueness
for b1, b2 being natural_equivalence of c4,c3 st ( for b3 being object of c1 holds b1 . b3 = (c5 ! b3) " ) & ( for b3 being object of c1 holds b2 . b3 = (c5 ! b3) " ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines " FUNCTOR3:def 6 :
for b1, b2 being category
for b3, b4 being covariant Functor of b1,b2
for b5 being natural_equivalence of b3,b4 st b3,b4 are_naturally_equivalent holds
for b6 being natural_equivalence of b4,b3 holds
( b6 = b5 " iff for b7 being object of b1 holds b6 . b7 = (b5 ! b7) " );

theorem Th38: :: FUNCTOR3:38
for b1, b2 being category
for b3, b4 being covariant Functor of b2,b1
for b5 being natural_equivalence of b3,b4
for b6 being object of b2 st b3,b4 are_naturally_equivalent holds
(b5 " ) ! b6 = (b5 ! b6) "
proof end;

theorem Th39: :: FUNCTOR3:39
for b1, b2 being category
for b3, b4 being covariant Functor of b1,b2
for b5 being natural_equivalence of b3,b4 st b3,b4 are_naturally_equivalent holds
b5 `*` (b5 " ) = idt b4
proof end;

theorem Th40: :: FUNCTOR3:40
for b1, b2 being category
for b3, b4 being covariant Functor of b1,b2
for b5 being natural_equivalence of b3,b4 st b3,b4 are_naturally_equivalent holds
(b5 " ) `*` b5 = idt b3
proof end;

definition
let c1, c2 be category;
let c3 be covariant Functor of c1,c2;
redefine func idt as idt c3 -> natural_equivalence of a3,a3;
coherence
idt c3 is natural_equivalence of c3,c3
proof end;
end;

theorem Th41: :: FUNCTOR3:41
for b1, b2 being category
for b3, b4 being covariant Functor of b1,b2
for b5 being natural_equivalence of b3,b4 st b3,b4 are_naturally_equivalent holds
(b5 " ) " = b5
proof end;

theorem Th42: :: FUNCTOR3:42
for b1, b2 being category
for b3, b4, b5 being covariant Functor of b1,b2
for b6 being natural_equivalence of b3,b5
for b7 being natural_equivalence of b5,b4
for b8 being natural_equivalence of b3,b4 st b8 = b7 `*` b6 & b3,b5 are_naturally_equivalent & b5,b4 are_naturally_equivalent holds
b8 " = (b6 " ) `*` (b7 " )
proof end;

theorem Th43: :: FUNCTOR3:43
for b1, b2 being category
for b3 being covariant Functor of b1,b2 holds (idt b3) " = idt b3
proof end;