:: CAT_2 semantic presentation

definition

let c₁ be non empty set ;
let c₂ be set ;
let c₃ be non empty set ;
let c₄ be FUNCTION_DOMAIN of c₂,c₃;
let c₅ be Function of c₁,c₄;
let c₆ be Element of c₁;
redefine func . as c₅ . c₆ -> Element of a₄;
coherence

proof end;

end;

theorem Th1: :: CAT_2:1

for b₁, b₂, b₃ being non empty set
for b₄ being Function of [:b₁,b₂:],b₃ holds curry b₄ is Function of b₁, Funcs b₂,b₃

proof end;

theorem Th2: :: CAT_2:2

for b₁, b₂, b₃ being non empty set
for b₄ being Function of [:b₂,b₁:],b₃ holds curry' b₄ is Function of b₁, Funcs b₂,b₃

proof end;

definition

let c₁, c₂, c₃ be non empty set ;
let c₄ be Function of [:c₁,c₂:],c₃;
redefine func curry as curry c₄ -> Function of a₁, Funcs a₂,a₃;
coherence by Th1;
redefine func curry' as curry' c₄ -> Function of a₂, Funcs a₁,a₃;
coherence by Th2;

end;

theorem Th3: :: CAT_2:3

for b₁, b₂, b₃ being non empty set
for b₄ being Element of b₁
for b₅ being Element of b₂
for b₆ being Function of [:b₁,b₂:],b₃ holds b₆ . [b₄,b₅] = ((curry b₆) . b₄) . b₅

proof end;

theorem Th4: :: CAT_2:4

for b₁, b₂, b₃ being non empty set
for b₄ being Element of b₁
for b₅ being Element of b₂
for b₆ being Function of [:b₁,b₂:],b₃ holds b₆ . [b₄,b₅] = ((curry' b₆) . b₅) . b₄

proof end;

definition

let c₁, c₂ be Category;
let c₃ be Object of c₂;
func c₁ --> c₃ -> Functor of a₁,a₂ equals :: CAT_2:def 1
the Morphisms of a₁ --> (id a₃);
coherence

proof end;

end;

:: deftheorem Def1 defines --> CAT_2:def 1 :

theorem Th5: :: CAT_2:5

canceled;

theorem Th6: :: CAT_2:6

for b₁, b₂ being Category
for b₃ being Object of b₁
for b₄ being Morphism of b₂ holds (b₂ --> b₃) . b₄ = id b₃ by FUNCOP_1:13;

theorem Th7: :: CAT_2:7

for b₁, b₂ being Category
for b₃ being Object of b₁
for b₄ being Object of b₂ holds (Obj (b₂ --> b₃)) . b₄ = b₃

proof end;

definition

let c₁, c₂ be Category;
func Funct c₁,c₂ -> set means :Def2: :: CAT_2:def 2
for b₁ being set holds
( b₁ in a₃ iff b₁ is Functor of a₁,a₂ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines Funct CAT_2:def 2 :

registration

let c₁, c₂ be Category;
cluster Funct a₁,a₂ -> non empty ;
coherence

proof end;

end;

definition

let c₁, c₂ be Category;
mode FUNCTOR-DOMAIN of c₁,c₂ -> non empty set means :Def3: :: CAT_2:def 3
for b₁ being Element of a₃ holds b₁ is Functor of a₁,a₂;
existence

proof end;

end;

:: deftheorem Def3 defines FUNCTOR-DOMAIN CAT_2:def 3 :

definition

let c₁, c₂ be Category;
let c₃ be FUNCTOR-DOMAIN of c₁,c₂;
redefine mode Element as Element of c₃ -> Functor of a₁,a₂;
coherence by Def3;

end;

definition

let c₁ be non empty set ;
let c₂, c₃ be Category;
let c₄ be FUNCTOR-DOMAIN of c₂,c₃;
let c₅ be Function of c₁,c₄;
let c₆ be Element of c₁;
redefine func . as c₅ . c₆ -> Element of a₄;
coherence

proof end;

end;

definition

let c₁, c₂ be Category;
redefine func Funct as Funct c₁,c₂ -> FUNCTOR-DOMAIN of a₁,a₂;
coherence

proof end;

end;

definition

let c₁ be Category;
mode Subcategory of c₁ -> Category means :Def4: :: CAT_2:def 4
( the Objects of a₂ c= the Objects of a₁ & ( for b₁, b₂ being Object of a₂
for b₃, b₄ being Object of a₁ st b₁ = b₃ & b₂ = b₄ holds
Hom b₁,b₂ c= Hom b₃,b₄ ) & the Comp of a₂ <= the Comp of a₁ & ( for b₁ being Object of a₂
for b₂ being Object of a₁ st b₁ = b₂ holds
id b₁ = id b₂ ) );
existence

proof end;

end;

:: deftheorem Def4 defines Subcategory CAT_2:def 4 :

registration

let c₁ be Category;
cluster strict Subcategory of a₁;
existence

proof end;

end;

theorem Th8: :: CAT_2:8

canceled;

theorem Th9: :: CAT_2:9

canceled;

theorem Th10: :: CAT_2:10

canceled;

theorem Th11: :: CAT_2:11

canceled;

theorem Th12: :: CAT_2:12

for b₁ being Category
for b₂ being Subcategory of b₁
for b₃ being Object of b₂ holds b₃ is Object of b₁

proof end;

theorem Th13: :: CAT_2:13

for b₁ being Category
for b₂ being Subcategory of b₁ holds the Morphisms of b₂ c= the Morphisms of b₁

proof end;

theorem Th14: :: CAT_2:14

for b₁ being Category
for b₂ being Subcategory of b₁
for b₃ being Morphism of b₂ holds b₃ is Morphism of b₁

proof end;

theorem Th15: :: CAT_2:15

for b₁ being Category
for b₂ being Subcategory of b₁
for b₃ being Morphism of b₂
for b₄ being Morphism of b₁ st b₃ = b₄ holds
( dom b₃ = dom b₄ & cod b₃ = cod b₄ )

proof end;

theorem Th16: :: CAT_2:16

for b₁ being Category
for b₂ being Subcategory of b₁
for b₃, b₄ being Object of b₂
for b₅, b₆ being Object of b₁
for b₇ being Morphism of b₃,b₄ st b₃ = b₅ & b₄ = b₆ & Hom b₃,b₄ <> {} holds
b₇ is Morphism of b₅,b₆

proof end;

theorem Th17: :: CAT_2:17

for b₁ being Category
for b₂ being Subcategory of b₁
for b₃, b₄ being Morphism of b₂
for b₅, b₆ being Morphism of b₁ st b₃ = b₅ & b₄ = b₆ & dom b₄ = cod b₃ holds
b₄ * b₃ = b₆ * b₅

proof end;

theorem Th18: :: CAT_2:18

for b₁ being Category holds b₁ is Subcategory of b₁

proof end;

theorem Th19: :: CAT_2:19

for b₁ being Category
for b₂ being Subcategory of b₁ holds id b₂ is Functor of b₂,b₁

proof end;

definition

let c₁ be Category;
let c₂ be Subcategory of c₁;
func incl c₂ -> Functor of a₂,a₁ equals :: CAT_2:def 5
id a₂;
coherence by Th19;

end;

:: deftheorem Def5 defines incl CAT_2:def 5 :

theorem Th20: :: CAT_2:20

canceled;

theorem Th21: :: CAT_2:21

for b₁ being Category
for b₂ being Subcategory of b₁
for b₃ being Morphism of b₂ holds (incl b₂) . b₃ = b₃ by CAT_1:115;

theorem Th22: :: CAT_2:22

for b₁ being Category
for b₂ being Subcategory of b₁
for b₃ being Object of b₂ holds (Obj (incl b₂)) . b₃ = b₃

proof end;

theorem Th23: :: CAT_2:23

for b₁ being Category
for b₂ being Subcategory of b₁
for b₃ being Object of b₂ holds (incl b₂) . b₃ = b₃ by Th22;

theorem Th24: :: CAT_2:24

for b₁ being Category
for b₂ being Subcategory of b₁ holds incl b₂ is faithful

proof end;

theorem Th25: :: CAT_2:25

for b₁ being Category
for b₂ being Subcategory of b₁ holds
( incl b₂ is full iff for b₃, b₄ being Object of b₂
for b₅, b₆ being Object of b₁ st b₃ = b₅ & b₄ = b₆ holds
Hom b₃,b₄ = Hom b₅,b₆ )

proof end;

definition

let c₁ be CatStr ;
let c₂ be Category;
pred c₁ is_full_subcategory_of c₂ means :Def6: :: CAT_2:def 6
( a₁ is Subcategory of a₂ & ( for b₁, b₂ being Object of a₁
for b₃, b₄ being Object of a₂ st b₁ = b₃ & b₂ = b₄ holds
Hom b₁,b₂ = Hom b₃,b₄ ) );

end;

:: deftheorem Def6 defines is_full_subcategory_of CAT_2:def 6 :

theorem Th26: :: CAT_2:26

canceled;

theorem Th27: :: CAT_2:27

for b₁ being Category
for b₂ being Subcategory of b₁ holds
( b₂ is_full_subcategory_of b₁ iff incl b₂ is full )

proof end;

theorem Th28: :: CAT_2:28

for b₁ being Category
for b₂ being non empty Subset of the Objects of b₁ holds union { (Hom b₃,b₄) where B is Object of b₁, B is Object of b₁ : ( b₃ in b₂ & b₄ in b₂ ) } is non empty Subset of the Morphisms of b₁

proof end;

theorem Th29: :: CAT_2:29

for b₁ being Category
for b₂ being non empty Subset of the Objects of b₁
for b₃ being non empty set st b₃ = union { (Hom b₄,b₅) where B is Object of b₁, B is Object of b₁ : ( b₄ in b₂ & b₅ in b₂ ) } holds
( the Dom of b₁ | b₃ is Function of b₃,b₂ & the Cod of b₁ | b₃ is Function of b₃,b₂ & the Comp of b₁ || b₃ is PartFunc of [:b₃,b₃:],b₃ & the Id of b₁ | b₂ is Function of b₂,b₃ )

proof end;

theorem Th30: :: CAT_2:30

for b₁ being Category
for b₂ being non empty Subset of the Objects of b₁
for b₃ being non empty set
for b₄, b₅ being Function of b₃,b₂
for b₆ being PartFunc of [:b₃,b₃:],b₃
for b₇ being Function of b₂,b₃ st b₃ = union { (Hom b₈,b₉) where B is Object of b₁, B is Object of b₁ : ( b₈ in b₂ & b₉ in b₂ ) } & b₄ = the Dom of b₁ | b₃ & b₅ = the Cod of b₁ | b₃ & b₆ = the Comp of b₁ || b₃ & b₇ = the Id of b₁ | b₂ holds
CatStr(# b₂,b₃,b₄,b₅,b₆,b₇ #) is_full_subcategory_of b₁

proof end;

theorem Th31: :: CAT_2:31

for b₁ being Category
for b₂ being non empty Subset of the Objects of b₁
for b₃ being non empty set
for b₄, b₅ being Function of b₃,b₂
for b₆ being PartFunc of [:b₃,b₃:],b₃
for b₇ being Function of b₂,b₃ st CatStr(# b₂,b₃,b₄,b₅,b₆,b₇ #) is_full_subcategory_of b₁ holds
( b₃ = union { (Hom b₈,b₉) where B is Object of b₁, B is Object of b₁ : ( b₈ in b₂ & b₉ in b₂ ) } & b₄ = the Dom of b₁ | b₃ & b₅ = the Cod of b₁ | b₃ & b₆ = the Comp of b₁ || b₃ & b₇ = the Id of b₁ | b₂ )

proof end;

definition

let c₁, c₂, c₃, c₄ be non empty set ;
let c₅ be Function of c₁,c₃;
let c₆ be Function of c₂,c₄;
redefine func [: as [:c₅,c₆:] -> Function of [:a₁,a₂:],[:a₃,a₄:];
coherence

proof end;

end;

definition

let c₁, c₂ be non empty set ;
let c₃ be PartFunc of [:c₁,c₁:],c₁;
let c₄ be PartFunc of [:c₂,c₂:],c₂;
redefine func |: as |:c₃,c₄:| -> PartFunc of [:[:a₁,a₂:],[:a₁,a₂:]:],[:a₁,a₂:];
coherence by FUNCT_4:62;

end;

definition

let c₁, c₂ be Category;
func [:c₁,c₂:] -> Category equals :: CAT_2:def 7
CatStr(# [:the Objects of a₁,the Objects of a₂:],[:the Morphisms of a₁,the Morphisms of a₂:],[:the Dom of a₁,the Dom of a₂:],[:the Cod of a₁,the Cod of a₂:],|:the Comp of a₁,the Comp of a₂:|,[:the Id of a₁,the Id of a₂:] #);
coherence

proof end;

end;

:: deftheorem Def7 defines [: CAT_2:def 7 :

registration

let c₁, c₂ be Category;
cluster [:a₁,a₂:] -> strict ;
coherence ;

end;

theorem Th32: :: CAT_2:32

canceled;

theorem Th33: :: CAT_2:33

for b₁, b₂ being Category holds
( the Objects of [:b₁,b₂:] = [:the Objects of b₁,the Objects of b₂:] & the Morphisms of [:b₁,b₂:] = [:the Morphisms of b₁,the Morphisms of b₂:] & the Dom of [:b₁,b₂:] = [:the Dom of b₁,the Dom of b₂:] & the Cod of [:b₁,b₂:] = [:the Cod of b₁,the Cod of b₂:] & the Comp of [:b₁,b₂:] = |:the Comp of b₁,the Comp of b₂:| & the Id of [:b₁,b₂:] = [:the Id of b₁,the Id of b₂:] ) ;

theorem Th34: :: CAT_2:34

for b₁, b₂ being Category
for b₃ being Object of b₁
for b₄ being Object of b₂ holds [b₃,b₄] is Object of [:b₁,b₂:] ;

definition

let c₁, c₂ be Category;
let c₃ be Object of c₁;
let c₄ be Object of c₂;
redefine func [ as [c₃,c₄] -> Object of [:a₁,a₂:];
coherence by Th34;

end;

theorem Th35: :: CAT_2:35

for b₁, b₂ being Category
for b₃ being Object of [:b₁,b₂:] ex b₄ being Object of b₁ex b₅ being Object of b₂ st b₃ = [b₄,b₅] by DOMAIN_1:9;

theorem Th36: :: CAT_2:36

for b₁, b₂ being Category
for b₃ being Morphism of b₁
for b₄ being Morphism of b₂ holds [b₃,b₄] is Morphism of [:b₁,b₂:] ;

definition

let c₁, c₂ be Category;
let c₃ be Morphism of c₁;
let c₄ be Morphism of c₂;
redefine func [ as [c₃,c₄] -> Morphism of [:a₁,a₂:];
coherence by Th36;

end;

theorem Th37: :: CAT_2:37

for b₁, b₂ being Category
for b₃ being Morphism of [:b₁,b₂:] ex b₄ being Morphism of b₁ex b₅ being Morphism of b₂ st b₃ = [b₄,b₅] by DOMAIN_1:9;

theorem Th38: :: CAT_2:38

for b₁, b₂ being Category
for b₃ being Morphism of b₁
for b₄ being Morphism of b₂ holds
( dom [b₃,b₄] = [(dom b₃),(dom b₄)] & cod [b₃,b₄] = [(cod b₃),(cod b₄)] ) by FUNCT_3:96;

theorem Th39: :: CAT_2:39

for b₁, b₂ being Category
for b₃, b₄ being Morphism of b₁
for b₅, b₆ being Morphism of b₂ st dom b₄ = cod b₃ & dom b₆ = cod b₅ holds
[b₄,b₆] * [b₃,b₅] = [(b₄ * b₃),(b₆ * b₅)]

proof end;

theorem Th40: :: CAT_2:40

for b₁, b₂ being Category
for b₃, b₄ being Morphism of b₁
for b₅, b₆ being Morphism of b₂ st dom [b₄,b₆] = cod [b₃,b₅] holds
[b₄,b₆] * [b₃,b₅] = [(b₄ * b₃),(b₆ * b₅)]

proof end;

theorem Th41: :: CAT_2:41

for b₁, b₂ being Category
for b₃ being Object of b₁
for b₄ being Object of b₂ holds id [b₃,b₄] = [(id b₃),(id b₄)] by FUNCT_3:96;

theorem Th42: :: CAT_2:42

for b₁, b₂ being Category
for b₃, b₄ being Object of b₁
for b₅, b₆ being Object of b₂ holds Hom [b₃,b₅],[b₄,b₆] = [:(Hom b₃,b₄),(Hom b₅,b₆):]

proof end;

theorem Th43: :: CAT_2:43

for b₁, b₂ being Category
for b₃, b₄ being Object of b₁
for b₅ being Morphism of b₃,b₄
for b₆, b₇ being Object of b₂
for b₈ being Morphism of b₆,b₇ st Hom b₃,b₄ <> {} & Hom b₆,b₇ <> {} holds
[b₅,b₈] is Morphism of [b₃,b₆],[b₄,b₇]

proof end;

theorem Th44: :: CAT_2:44

for b₁, b₂, b₃ being Category
for b₄ being Functor of [:b₁,b₂:],b₃
for b₅ being Object of b₁ holds (curry b₄) . (id b₅) is Functor of b₂,b₃

proof end;

theorem Th45: :: CAT_2:45

for b₁, b₂, b₃ being Category
for b₄ being Functor of [:b₁,b₂:],b₃
for b₅ being Object of b₂ holds (curry' b₄) . (id b₅) is Functor of b₁,b₃

proof end;

definition

let c₁, c₂, c₃ be Category;
let c₄ be Functor of [:c₁,c₂:],c₃;
let c₅ be Object of c₁;
func c₄ ?- c₅ -> Functor of a₂,a₃ equals :: CAT_2:def 8
(curry a₄) . (id a₅);
coherence by Th44;

end;

:: deftheorem Def8 defines ?- CAT_2:def 8 :

theorem Th46: :: CAT_2:46

canceled;

theorem Th47: :: CAT_2:47

for b₁, b₂, b₃ being Category
for b₄ being Functor of [:b₁,b₂:],b₃
for b₅ being Object of b₁
for b₆ being Morphism of b₂ holds (b₄ ?- b₅) . b₆ = b₄ . [(id b₅),b₆] by Th3;

theorem Th48: :: CAT_2:48

for b₁, b₂, b₃ being Category
for b₄ being Functor of [:b₁,b₂:],b₃
for b₅ being Object of b₁
for b₆ being Object of b₂ holds (Obj (b₄ ?- b₅)) . b₆ = (Obj b₄) . [b₅,b₆]

proof end;

definition

let c₁, c₂, c₃ be Category;
let c₄ be Functor of [:c₁,c₂:],c₃;
let c₅ be Object of c₂;
func c₄ -? c₅ -> Functor of a₁,a₃ equals :: CAT_2:def 9
(curry' a₄) . (id a₅);
coherence by Th45;

end;

:: deftheorem Def9 defines -? CAT_2:def 9 :

theorem Th49: :: CAT_2:49

canceled;

theorem Th50: :: CAT_2:50

for b₁, b₂, b₃ being Category
for b₄ being Functor of [:b₁,b₂:],b₃
for b₅ being Object of b₂
for b₆ being Morphism of b₁ holds (b₄ -? b₅) . b₆ = b₄ . [b₆,(id b₅)] by Th4;

theorem Th51: :: CAT_2:51

for b₁, b₂, b₃ being Category
for b₄ being Functor of [:b₁,b₂:],b₃
for b₅ being Object of b₁
for b₆ being Object of b₂ holds (Obj (b₄ -? b₆)) . b₅ = (Obj b₄) . [b₅,b₆]

proof end;

theorem Th52: :: CAT_2:52

for b₁, b₂, b₃ being Category
for b₄ being Function of the Objects of b₁, Funct b₂,b₃
for b₅ being Function of the Objects of b₂, Funct b₁,b₃ st ( for b₆ being Object of b₁
for b₇ being Object of b₂ holds (b₅ . b₇) . (id b₆) = (b₄ . b₆) . (id b₇) ) & ( for b₆ being Morphism of b₂
for b₇ being Morphism of b₁ holds ((b₅ . (cod b₆)) . b₇) * ((b₄ . (dom b₇)) . b₆) = ((b₄ . (cod b₇)) . b₆) * ((b₅ . (dom b₆)) . b₇) ) holds
ex b₆ being Functor of [:b₂,b₁:],b₃ st
for b₇ being Morphism of b₂
for b₈ being Morphism of b₁ holds b₆ . [b₇,b₈] = ((b₄ . (cod b₈)) . b₇) * ((b₅ . (dom b₇)) . b₈)

proof end;

theorem Th53: :: CAT_2:53

for b₁, b₂, b₃ being Category
for b₄ being Function of the Objects of b₁, Funct b₂,b₃
for b₅ being Function of the Objects of b₂, Funct b₁,b₃ st ex b₆ being Functor of [:b₂,b₁:],b₃ st
for b₇ being Object of b₁
for b₈ being Object of b₂ holds
( b₆ -? b₇ = b₄ . b₇ & b₆ ?- b₈ = b₅ . b₈ ) holds
for b₆ being Morphism of b₂
for b₇ being Morphism of b₁ holds ((b₅ . (cod b₆)) . b₇) * ((b₄ . (dom b₇)) . b₆) = ((b₄ . (cod b₇)) . b₆) * ((b₅ . (dom b₆)) . b₇)

proof end;

theorem Th54: :: CAT_2:54

for b₁, b₂ being Category holds pr1 the Morphisms of b₁,the Morphisms of b₂ is Functor of [:b₁,b₂:],b₁

proof end;

theorem Th55: :: CAT_2:55

for b₁, b₂ being Category holds pr2 the Morphisms of b₁,the Morphisms of b₂ is Functor of [:b₁,b₂:],b₂

proof end;

definition

let c₁, c₂ be Category;
func pr1 c₁,c₂ -> Functor of [:a₁,a₂:],a₁ equals :: CAT_2:def 10
pr1 the Morphisms of a₁,the Morphisms of a₂;
coherence by Th54;
func pr2 c₁,c₂ -> Functor of [:a₁,a₂:],a₂ equals :: CAT_2:def 11
pr2 the Morphisms of a₁,the Morphisms of a₂;
coherence by Th55;

end;

:: deftheorem Def10 defines pr1 CAT_2:def 10 :

:: deftheorem Def11 defines pr2 CAT_2:def 11 :

theorem Th56: :: CAT_2:56

canceled;

theorem Th57: :: CAT_2:57

canceled;

theorem Th58: :: CAT_2:58

for b₁, b₂ being Category
for b₃ being Morphism of b₁
for b₄ being Morphism of b₂ holds (pr1 b₁,b₂) . [b₃,b₄] = b₃ by FUNCT_3:def 5;

theorem Th59: :: CAT_2:59

for b₁, b₂ being Category
for b₃ being Object of b₁
for b₄ being Object of b₂ holds (Obj (pr1 b₁,b₂)) . [b₃,b₄] = b₃

proof end;

theorem Th60: :: CAT_2:60

for b₁, b₂ being Category
for b₃ being Morphism of b₁
for b₄ being Morphism of b₂ holds (pr2 b₁,b₂) . [b₃,b₄] = b₄ by FUNCT_3:def 6;

theorem Th61: :: CAT_2:61

for b₁, b₂ being Category
for b₃ being Object of b₁
for b₄ being Object of b₂ holds (Obj (pr2 b₁,b₂)) . [b₃,b₄] = b₄

proof end;

theorem Th62: :: CAT_2:62

for b₁, b₂, b₃ being Category
for b₄ being Functor of b₁,b₂
for b₅ being Functor of b₁,b₃ holds <:b₄,b₅:> is Functor of b₁,[:b₂,b₃:]

proof end;

definition

let c₁, c₂, c₃ be Category;
let c₄ be Functor of c₁,c₂;
let c₅ be Functor of c₁,c₃;
redefine func <: as <:c₄,c₅:> -> Functor of a₁,[:a₂,a₃:];
coherence by Th62;

end;

theorem Th63: :: CAT_2:63

for b₁, b₂, b₃ being Category
for b₄ being Functor of b₁,b₂
for b₅ being Functor of b₁,b₃
for b₆ being Object of b₁ holds (Obj <:b₄,b₅:>) . b₆ = [((Obj b₄) . b₆),((Obj b₅) . b₆)]

proof end;

theorem Th64: :: CAT_2:64

for b₁, b₂, b₃, b₄ being Category
for b₅ being Functor of b₁,b₂
for b₆ being Functor of b₃,b₄ holds [:b₅,b₆:] = <:(b₅ * (pr1 b₁,b₃)),(b₆ * (pr2 b₁,b₃)):>

proof end;

theorem Th65: :: CAT_2:65

for b₁, b₂, b₃, b₄ being Category
for b₅ being Functor of b₁,b₂
for b₆ being Functor of b₃,b₄ holds [:b₅,b₆:] is Functor of [:b₁,b₃:],[:b₂,b₄:]

proof end;

definition

let c₁, c₂, c₃, c₄ be Category;
let c₅ be Functor of c₁,c₃;
let c₆ be Functor of c₂,c₄;
redefine func [: as [:c₅,c₆:] -> Functor of [:a₁,a₂:],[:a₃,a₄:];
coherence by Th65;

end;

theorem Th66: :: CAT_2:66

for b₁, b₂, b₃, b₄ being Category
for b₅ being Functor of b₁,b₂
for b₆ being Functor of b₃,b₄
for b₇ being Object of b₁
for b₈ being Object of b₃ holds (Obj [:b₅,b₆:]) . [b₇,b₈] = [((Obj b₅) . b₇),((Obj b₆) . b₈)]

proof end;