:: CAT_2 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
let D be non empty set ;
let X be set ;
let E be non empty set ;
let F be FUNCTION_DOMAIN of X,E;
let f be Function of D,F;
let d be Element of D;
:: original: .
redefine func f . d -> Element of F;
coherence
f . d is Element of F
proof end;
end;

theorem Th1: :: CAT_2:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, D, E being non empty set
for f being Function of [:C,D:],E holds curry f is Function of C, Funcs D,E
proof end;

theorem Th2: :: CAT_2:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D, C, E being non empty set
for f being Function of [:C,D:],E holds curry' f is Function of D, Funcs C,E
proof end;

definition
let C, D, E be non empty set ;
let f be Function of [:C,D:],E;
:: original: curry
redefine func curry f -> Function of C, Funcs D,E;
coherence
curry f is Function of C, Funcs D,E
by Th1;
:: original: curry'
redefine func curry' f -> Function of D, Funcs C,E;
coherence
curry' f is Function of D, Funcs C,E
by Th2;
end;

theorem Th3: :: CAT_2:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, D, E being non empty set
for c being Element of C
for d being Element of D
for f being Function of [:C,D:],E holds f . [c,d] = ((curry f) . c) . d
proof end;

theorem Th4: :: CAT_2:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, D, E being non empty set
for c being Element of C
for d being Element of D
for f being Function of [:C,D:],E holds f . [c,d] = ((curry' f) . d) . c
proof end;

definition
let B, C be Category;
let c be Object of C;
func B --> c -> Functor of B,C equals :: CAT_2:def 1
the Morphisms of B --> (id c);
coherence
the Morphisms of B --> (id c) is Functor of B,C
proof end;
end;

:: deftheorem defines --> CAT_2:def 1 :
for B, C being Category
for c being Object of C holds B --> c = the Morphisms of B --> (id c);

theorem :: CAT_2:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th6: :: CAT_2:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, B being Category
for c being Object of C
for f being Morphism of B holds (B --> c) . f = id c by FUNCOP_1:13;

theorem :: CAT_2:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, B being Category
for c being Object of C
for b being Object of B holds (Obj (B --> c)) . b = c
proof end;

definition
let C, D be Category;
func Funct C,D -> set means :Def2: :: CAT_2:def 2
for x being set holds
( x in it iff x is Functor of C,D );
existence
ex b1 being set st
for x being set holds
( x in b1 iff x is Functor of C,D )
proof end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff x is Functor of C,D ) ) & ( for x being set holds
( x in b2 iff x is Functor of C,D ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines Funct CAT_2:def 2 :
for C, D being Category
for b3 being set holds
( b3 = Funct C,D iff for x being set holds
( x in b3 iff x is Functor of C,D ) );

registration
let C, D be Category;
cluster Funct C,D -> non empty ;
coherence
not Funct C,D is empty
proof end;
end;

definition
let C, D be Category;
mode FUNCTOR-DOMAIN of C,D -> non empty set means :Def3: :: CAT_2:def 3
for x being Element of it holds x is Functor of C,D;
existence
ex b1 being non empty set st
for x being Element of b1 holds x is Functor of C,D
proof end;
end;

:: deftheorem Def3 defines FUNCTOR-DOMAIN CAT_2:def 3 :
for C, D being Category
for b3 being non empty set holds
( b3 is FUNCTOR-DOMAIN of C,D iff for x being Element of b3 holds x is Functor of C,D );

definition
let C, D be Category;
let F be FUNCTOR-DOMAIN of C,D;
:: original: Element
redefine mode Element of F -> Functor of C,D;
coherence
for b1 being Element of F holds b1 is Functor of C,D
by Def3;
end;

definition
let A be non empty set ;
let C, D be Category;
let F be FUNCTOR-DOMAIN of C,D;
let T be Function of A,F;
let x be Element of A;
:: original: .
redefine func T . x -> Element of F;
coherence
T . x is Element of F
proof end;
end;

definition
let C, D be Category;
:: original: Funct
redefine func Funct C,D -> FUNCTOR-DOMAIN of C,D;
coherence
Funct C,D is FUNCTOR-DOMAIN of C,D
proof end;
end;

definition
let C be Category;
mode Subcategory of C -> Category means :Def4: :: CAT_2:def 4
( the Objects of it c= the Objects of C & ( for a, b being Object of it
for a', b' being Object of C st a = a' & b = b' holds
Hom a,b c= Hom a',b' ) & the Comp of it <= the Comp of C & ( for a being Object of it
for a' being Object of C st a = a' holds
id a = id a' ) );
existence
ex b1 being Category st
( the Objects of b1 c= the Objects of C & ( for a, b being Object of b1
for a', b' being Object of C st a = a' & b = b' holds
Hom a,b c= Hom a',b' ) & the Comp of b1 <= the Comp of C & ( for a being Object of b1
for a' being Object of C st a = a' holds
id a = id a' ) )
proof end;
end;

:: deftheorem Def4 defines Subcategory CAT_2:def 4 :
for C, b2 being Category holds
( b2 is Subcategory of C iff ( the Objects of b2 c= the Objects of C & ( for a, b being Object of b2
for a', b' being Object of C st a = a' & b = b' holds
Hom a,b c= Hom a',b' ) & the Comp of b2 <= the Comp of C & ( for a being Object of b2
for a' being Object of C st a = a' holds
id a = id a' ) ) );

registration
let C be Category;
cluster strict Subcategory of C;
existence
ex b1 being Subcategory of C st b1 is strict
proof end;
end;

theorem :: CAT_2:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: CAT_2:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: CAT_2:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: CAT_2:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th12: :: CAT_2:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for E being Subcategory of C
for e being Object of E holds e is Object of C
proof end;

theorem Th13: :: CAT_2:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for E being Subcategory of C holds the Morphisms of E c= the Morphisms of C
proof end;

theorem Th14: :: CAT_2:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for E being Subcategory of C
for f being Morphism of E holds f is Morphism of C
proof end;

theorem Th15: :: CAT_2:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for E being Subcategory of C
for f being Morphism of E
for f' being Morphism of C st f = f' holds
( dom f = dom f' & cod f = cod f' )
proof end;

theorem :: CAT_2:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for E being Subcategory of C
for a, b being Object of E
for a', b' being Object of C
for f being Morphism of a,b st a = a' & b = b' & Hom a,b <> {} holds
f is Morphism of a',b'
proof end;

theorem Th17: :: CAT_2:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for E being Subcategory of C
for f, g being Morphism of E
for f', g' being Morphism of C st f = f' & g = g' & dom g = cod f holds
g * f = g' * f'
proof end;

theorem :: CAT_2:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category holds C is Subcategory of C
proof end;

theorem Th19: :: CAT_2:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for E being Subcategory of C holds id E is Functor of E,C
proof end;

definition
let C be Category;
let E be Subcategory of C;
func incl E -> Functor of E,C equals :: CAT_2:def 5
id E;
coherence
id E is Functor of E,C
by Th19;
end;

:: deftheorem defines incl CAT_2:def 5 :
for C being Category
for E being Subcategory of C holds incl E = id E;

theorem :: CAT_2:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th21: :: CAT_2:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for E being Subcategory of C
for f being Morphism of E holds (incl E) . f = f by CAT_1:115;

theorem Th22: :: CAT_2:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for E being Subcategory of C
for a being Object of E holds (Obj (incl E)) . a = a
proof end;

theorem Th23: :: CAT_2:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for E being Subcategory of C
for a being Object of E holds (incl E) . a = a by Th22;

theorem :: CAT_2:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for E being Subcategory of C holds incl E is faithful
proof end;

theorem Th25: :: CAT_2:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for E being Subcategory of C holds
( incl E is full iff for a, b being Object of E
for a', b' being Object of C st a = a' & b = b' holds
Hom a,b = Hom a',b' )
proof end;

definition
let C be CatStr ;
let D be Category;
pred C is_full_subcategory_of D means :Def6: :: CAT_2:def 6
( C is Subcategory of D & ( for a, b being Object of C
for a', b' being Object of D st a = a' & b = b' holds
Hom a,b = Hom a',b' ) );
end;

:: deftheorem Def6 defines is_full_subcategory_of CAT_2:def 6 :
for C being CatStr
for D being Category holds
( C is_full_subcategory_of D iff ( C is Subcategory of D & ( for a, b being Object of C
for a', b' being Object of D st a = a' & b = b' holds
Hom a,b = Hom a',b' ) ) );

theorem :: CAT_2:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: CAT_2:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for E being Subcategory of C holds
( E is_full_subcategory_of C iff incl E is full )
proof end;

theorem Th28: :: CAT_2:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for O being non empty Subset of the Objects of C holds union { (Hom a,b) where a, b is Object of C : ( a in O & b in O ) } is non empty Subset of the Morphisms of C
proof end;

theorem Th29: :: CAT_2:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for O being non empty Subset of the Objects of C
for M being non empty set st M = union { (Hom a,b) where a, b is Object of C : ( a in O & b in O ) } holds
( the Dom of C | M is Function of M,O & the Cod of C | M is Function of M,O & the Comp of C || M is PartFunc of [:M,M:],M & the Id of C | O is Function of O,M )
proof end;

theorem :: CAT_2:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for O being non empty Subset of the Objects of C
for M being non empty set
for d, c being Function of M,O
for p being PartFunc of [:M,M:],M
for i being Function of O,M st M = union { (Hom a,b) where a, b is Object of C : ( a in O & b in O ) } & d = the Dom of C | M & c = the Cod of C | M & p = the Comp of C || M & i = the Id of C | O holds
CatStr(# O,M,d,c,p,i #) is_full_subcategory_of C
proof end;

theorem :: CAT_2:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for O being non empty Subset of the Objects of C
for M being non empty set
for d, c being Function of M,O
for p being PartFunc of [:M,M:],M
for i being Function of O,M st CatStr(# O,M,d,c,p,i #) is_full_subcategory_of C holds
( M = union { (Hom a,b) where a, b is Object of C : ( a in O & b in O ) } & d = the Dom of C | M & c = the Cod of C | M & p = the Comp of C || M & i = the Id of C | O )
proof end;

definition
let X1, X2, Y1, Y2 be non empty set ;
let f1 be Function of X1,Y1;
let f2 be Function of X2,Y2;
:: original: [:
redefine func [:f1,f2:] -> Function of [:X1,X2:],[:Y1,Y2:];
coherence
[:f1,f2:] is Function of [:X1,X2:],[:Y1,Y2:]
proof end;
end;

definition
let A, B be non empty set ;
let f be PartFunc of [:A,A:],A;
let g be PartFunc of [:B,B:],B;
:: original: |:
redefine func |:f,g:| -> PartFunc of [:[:A,B:],[:A,B:]:],[:A,B:];
coherence
|:f,g:| is PartFunc of [:[:A,B:],[:A,B:]:],[:A,B:]
by FUNCT_4:62;
end;

definition
let C, D be Category;
func [:C,D:] -> Category equals :: CAT_2:def 7
CatStr(# [:the Objects of C,the Objects of D:],[:the Morphisms of C,the Morphisms of D:],[:the Dom of C,the Dom of D:],[:the Cod of C,the Cod of D:],|:the Comp of C,the Comp of D:|,[:the Id of C,the Id of D:] #);
coherence
CatStr(# [:the Objects of C,the Objects of D:],[:the Morphisms of C,the Morphisms of D:],[:the Dom of C,the Dom of D:],[:the Cod of C,the Cod of D:],|:the Comp of C,the Comp of D:|,[:the Id of C,the Id of D:] #) is Category
proof end;
end;

:: deftheorem defines [: CAT_2:def 7 :
for C, D being Category holds [:C,D:] = CatStr(# [:the Objects of C,the Objects of D:],[:the Morphisms of C,the Morphisms of D:],[:the Dom of C,the Dom of D:],[:the Cod of C,the Cod of D:],|:the Comp of C,the Comp of D:|,[:the Id of C,the Id of D:] #);

registration
let C, D be Category;
cluster [:C,D:] -> strict ;
coherence
[:C,D:] is strict
;
end;

theorem :: CAT_2:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: CAT_2:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, D being Category holds
( the Objects of [:C,D:] = [:the Objects of C,the Objects of D:] & the Morphisms of [:C,D:] = [:the Morphisms of C,the Morphisms of D:] & the Dom of [:C,D:] = [:the Dom of C,the Dom of D:] & the Cod of [:C,D:] = [:the Cod of C,the Cod of D:] & the Comp of [:C,D:] = |:the Comp of C,the Comp of D:| & the Id of [:C,D:] = [:the Id of C,the Id of D:] ) ;

theorem Th34: :: CAT_2:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, D being Category
for c being Object of C
for d being Object of D holds [c,d] is Object of [:C,D:] ;

definition
let C, D be Category;
let c be Object of C;
let d be Object of D;
:: original: [
redefine func [c,d] -> Object of [:C,D:];
coherence
[c,d] is Object of [:C,D:]
by Th34;
end;

theorem Th35: :: CAT_2:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, D being Category
for cd being Object of [:C,D:] ex c being Object of C ex d being Object of D st cd = [c,d] by DOMAIN_1:9;

theorem Th36: :: CAT_2:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, D being Category
for f being Morphism of C
for g being Morphism of D holds [f,g] is Morphism of [:C,D:] ;

definition
let C, D be Category;
let f be Morphism of C;
let g be Morphism of D;
:: original: [
redefine func [f,g] -> Morphism of [:C,D:];
coherence
[f,g] is Morphism of [:C,D:]
by Th36;
end;

theorem Th37: :: CAT_2:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, D being Category
for fg being Morphism of [:C,D:] ex f being Morphism of C ex g being Morphism of D st fg = [f,g] by DOMAIN_1:9;

theorem Th38: :: CAT_2:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, D being Category
for f being Morphism of C
for g being Morphism of D holds
( dom [f,g] = [(dom f),(dom g)] & cod [f,g] = [(cod f),(cod g)] ) by FUNCT_3:96;

theorem Th39: :: CAT_2:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, D being Category
for f, f' being Morphism of C
for g, g' being Morphism of D st dom f' = cod f & dom g' = cod g holds
[f',g'] * [f,g] = [(f' * f),(g' * g)]
proof end;

theorem Th40: :: CAT_2:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, D being Category
for f, f' being Morphism of C
for g, g' being Morphism of D st dom [f',g'] = cod [f,g] holds
[f',g'] * [f,g] = [(f' * f),(g' * g)]
proof end;

theorem Th41: :: CAT_2:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, D being Category
for c being Object of C
for d being Object of D holds id [c,d] = [(id c),(id d)] by FUNCT_3:96;

theorem :: CAT_2:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, D being Category
for c, c' being Object of C
for d, d' being Object of D holds Hom [c,d],[c',d'] = [:(Hom c,c'),(Hom d,d'):]
proof end;

theorem :: CAT_2:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, D being Category
for c, c' being Object of C
for f being Morphism of c,c'
for d, d' being Object of D
for g being Morphism of d,d' st Hom c,c' <> {} & Hom d,d' <> {} holds
[f,g] is Morphism of [c,d],[c',d']
proof end;

theorem Th44: :: CAT_2:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, C', D being Category
for S being Functor of [:C,C':],D
for c being Object of C holds (curry S) . (id c) is Functor of C',D
proof end;

theorem Th45: :: CAT_2:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, C', D being Category
for S being Functor of [:C,C':],D
for c' being Object of C' holds (curry' S) . (id c') is Functor of C,D
proof end;

definition
let C, C', D be Category;
let S be Functor of [:C,C':],D;
let c be Object of C;
func S ?- c -> Functor of C',D equals :: CAT_2:def 8
(curry S) . (id c);
coherence
(curry S) . (id c) is Functor of C',D
by Th44;
end;

:: deftheorem defines ?- CAT_2:def 8 :
for C, C', D being Category
for S being Functor of [:C,C':],D
for c being Object of C holds S ?- c = (curry S) . (id c);

theorem :: CAT_2:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th47: :: CAT_2:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, C', D being Category
for S being Functor of [:C,C':],D
for c being Object of C
for f being Morphism of C' holds (S ?- c) . f = S . [(id c),f] by Th3;

theorem :: CAT_2:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, C', D being Category
for S being Functor of [:C,C':],D
for c being Object of C
for c' being Object of C' holds (Obj (S ?- c)) . c' = (Obj S) . [c,c']
proof end;

definition
let C, C', D be Category;
let S be Functor of [:C,C':],D;
let c' be Object of C';
func S -? c' -> Functor of C,D equals :: CAT_2:def 9
(curry' S) . (id c');
coherence
(curry' S) . (id c') is Functor of C,D
by Th45;
end;

:: deftheorem defines -? CAT_2:def 9 :
for C, C', D being Category
for S being Functor of [:C,C':],D
for c' being Object of C' holds S -? c' = (curry' S) . (id c');

theorem :: CAT_2:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th50: :: CAT_2:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, C', D being Category
for S being Functor of [:C,C':],D
for c' being Object of C'
for f being Morphism of C holds (S -? c') . f = S . [f,(id c')] by Th4;

theorem :: CAT_2:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, C', D being Category
for S being Functor of [:C,C':],D
for c being Object of C
for c' being Object of C' holds (Obj (S -? c')) . c = (Obj S) . [c,c']
proof end;

theorem :: CAT_2:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, B, D being Category
for L being Function of the Objects of C, Funct B,D
for M being Function of the Objects of B, Funct C,D st ( for c being Object of C
for b being Object of B holds (M . b) . (id c) = (L . c) . (id b) ) & ( for f being Morphism of B
for g being Morphism of C holds ((M . (cod f)) . g) * ((L . (dom g)) . f) = ((L . (cod g)) . f) * ((M . (dom f)) . g) ) holds
ex S being Functor of [:B,C:],D st
for f being Morphism of B
for g being Morphism of C holds S . [f,g] = ((L . (cod g)) . f) * ((M . (dom f)) . g)
proof end;

theorem :: CAT_2:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, B, D being Category
for L being Function of the Objects of C, Funct B,D
for M being Function of the Objects of B, Funct C,D st ex S being Functor of [:B,C:],D st
for c being Object of C
for b being Object of B holds
( S -? c = L . c & S ?- b = M . b ) holds
for f being Morphism of B
for g being Morphism of C holds ((M . (cod f)) . g) * ((L . (dom g)) . f) = ((L . (cod g)) . f) * ((M . (dom f)) . g)
proof end;

theorem Th54: :: CAT_2:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, D being Category holds pr1 the Morphisms of C,the Morphisms of D is Functor of [:C,D:],C
proof end;

theorem Th55: :: CAT_2:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, D being Category holds pr2 the Morphisms of C,the Morphisms of D is Functor of [:C,D:],D
proof end;

definition
let C, D be Category;
func pr1 C,D -> Functor of [:C,D:],C equals :: CAT_2:def 10
pr1 the Morphisms of C,the Morphisms of D;
coherence
pr1 the Morphisms of C,the Morphisms of D is Functor of [:C,D:],C
by Th54;
func pr2 C,D -> Functor of [:C,D:],D equals :: CAT_2:def 11
pr2 the Morphisms of C,the Morphisms of D;
coherence
pr2 the Morphisms of C,the Morphisms of D is Functor of [:C,D:],D
by Th55;
end;

:: deftheorem defines pr1 CAT_2:def 10 :
for C, D being Category holds pr1 C,D = pr1 the Morphisms of C,the Morphisms of D;

:: deftheorem defines pr2 CAT_2:def 11 :
for C, D being Category holds pr2 C,D = pr2 the Morphisms of C,the Morphisms of D;

theorem :: CAT_2:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: CAT_2:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th58: :: CAT_2:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, D being Category
for f being Morphism of C
for g being Morphism of D holds (pr1 C,D) . [f,g] = f by FUNCT_3:def 5;

theorem :: CAT_2:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, D being Category
for c being Object of C
for d being Object of D holds (Obj (pr1 C,D)) . [c,d] = c
proof end;

theorem Th60: :: CAT_2:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, D being Category
for f being Morphism of C
for g being Morphism of D holds (pr2 C,D) . [f,g] = g by FUNCT_3:def 6;

theorem :: CAT_2:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, D being Category
for c being Object of C
for d being Object of D holds (Obj (pr2 C,D)) . [c,d] = d
proof end;

theorem Th62: :: CAT_2:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, D, D' being Category
for T being Functor of C,D
for T' being Functor of C,D' holds <:T,T':> is Functor of C,[:D,D':]
proof end;

definition
let C, D, D' be Category;
let T be Functor of C,D;
let T' be Functor of C,D';
:: original: <:
redefine func <:T,T':> -> Functor of C,[:D,D':];
coherence
<:T,T':> is Functor of C,[:D,D':]
by Th62;
end;

theorem :: CAT_2:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, D, D' being Category
for T being Functor of C,D
for T' being Functor of C,D'
for c being Object of C holds (Obj <:T,T':>) . c = [((Obj T) . c),((Obj T') . c)]
proof end;

theorem Th64: :: CAT_2:64  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, D, C', D' being Category
for T being Functor of C,D
for T' being Functor of C',D' holds [:T,T':] = <:(T * (pr1 C,C')),(T' * (pr2 C,C')):>
proof end;

theorem Th65: :: CAT_2:65  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, D, C', D' being Category
for T being Functor of C,D
for T' being Functor of C',D' holds [:T,T':] is Functor of [:C,C':],[:D,D':]
proof end;

definition
let C, C', D, D' be Category;
let T be Functor of C,D;
let T' be Functor of C',D';
:: original: [:
redefine func [:T,T':] -> Functor of [:C,C':],[:D,D':];
coherence
[:T,T':] is Functor of [:C,C':],[:D,D':]
by Th65;
end;

theorem :: CAT_2:66  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, D, C', D' being Category
for T being Functor of C,D
for T' being Functor of C',D'
for c being Object of C
for c' being Object of C' holds (Obj [:T,T':]) . [c,c'] = [((Obj T) . c),((Obj T') . c')]
proof end;