:: CAT_2 semantic presentation

begin

theorem :: CAT_2:1
canceled;

theorem :: CAT_2:2
canceled;

theorem :: CAT_2:3
canceled;

theorem :: CAT_2:4
canceled;


definition
let B, C be Category;
let c be Object of C;
funcB --> c ->  Functor of B,C equals :: CAT_2:def 1
 the carrier' of B --> (id c);
coherence
 the carrier' of B --> (id c) is Functor of B,C
proof
reconsider T = the carrier' of B --> (id c) as Function of the carrier' of B, the carrier' of C ;
now__::_thesis:_(_(_for_b_being_Object_of_B_ex_d_being_Object_of_C_st_T_._(id_b)_=_id_d_)_&_(_for_f_being_Morphism_of_B_holds_
(_T_._(id_(dom_f))_=_id_(dom_(T_._f))_&_T_._(id_(cod_f))_=_id_(cod_(T_._f))_)_)_&_(_for_f,_g_being_Morphism_of_B_st_dom_g_=_cod_f_holds_
T_._(g_(*)_f)_=_(T_._g)_(*)_(T_._f)_)_)
thus  for b being Object of B ex d being Object of C st T . (id b) = id d by FUNCOP_1:7; ::_thesis: ( ( for f being Morphism of B holds
( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) ) ) & ( for f, g being Morphism of B st dom g = cod f holds
T . (g (*) f) = (T . g) (*) (T . f) ) )
thus  for f being Morphism of B holds
( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) ) ::_thesis: for f, g being Morphism of B st dom g = cod f holds
T . (g (*) f) = (T . g) (*) (T . f)
proof
let f be Morphism of B; ::_thesis: ( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) )
 T . (id (cod f)) = id c by FUNCOP_1:7;
then A1: T . (id (cod f)) = id (cod (id c)) ;
 T . (id (dom f)) = id c by FUNCOP_1:7;
then  T . (id (dom f)) = id (dom (id c)) ;
hence  ( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) ) by A1, FUNCOP_1:7; ::_thesis: verum
end;
let f, g be Morphism of B; ::_thesis: ( dom g = cod f implies T . (g (*) f) = (T . g) (*) (T . f) )
assume  dom g = cod f ; ::_thesis: T . (g (*) f) = (T . g) (*) (T . f)
 Hom (c,c) <> {} ;
then A2: ( T . f = id c & (id c) * (id c) = (id c) (*) (id c) ) by CAT_1:def_13, FUNCOP_1:7;
 ( T . (g (*) f) = id c & T . g = id c ) by FUNCOP_1:7;
hence  T . (g (*) f) = (T . g) (*) (T . f) by A2; ::_thesis: verum
end;
hence  the carrier' of B --> (id c) is Functor of B,C by CAT_1:61; ::_thesis: verum
end;
end;

:: deftheorem  defines --> CAT_2:def_1_:_
 for B, C being Category
for c being Object of C holds B --> c = the carrier' of B --> (id c);

theorem :: CAT_2:5
for C, B being Category
for c being Object of C
for b being Object of B holds (Obj (B --> c)) . b = c
proof
let C, B be Category; ::_thesis: for c being Object of C
for b being Object of B holds (Obj (B --> c)) . b = c
let c be Object of C; ::_thesis: for b being Object of B holds (Obj (B --> c)) . b = c
let b be Object of B; ::_thesis: (Obj (B --> c)) . b = c
 (B --> c) . (id b) = id c by FUNCOP_1:7;
hence  (Obj (B --> c)) . b = c by CAT_1:67; ::_thesis: verum
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
defpred S1[ set ] means $1 is Functor of C,D;
consider F being set  such that
A1: for x being set holds
( x in F iff ( x in Funcs ( the carrier' of C, the carrier' of D) & S1[x] ) ) from XBOOLE_0:sch_1();
take  F ; ::_thesis: for x being set holds
( x in F iff x is Functor of C,D )
let x be set ; ::_thesis: ( x in F iff x is Functor of C,D )
thus  ( x in F implies x is Functor of C,D ) by A1; ::_thesis: ( x is Functor of C,D implies x in F )
assume A2: x is Functor of C,D ; ::_thesis: x in F
then  x in Funcs ( the carrier' of C, the carrier' of D) by FUNCT_2:8;
hence  x in F by A1, A2; ::_thesis: verum
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
let F1, F2 be set ; ::_thesis: ( ( for x being set holds
( x in F1 iff x is Functor of C,D ) ) & ( for x being set holds
( x in F2 iff x is Functor of C,D ) ) implies F1 = F2 )
assume that
A3: for x being set holds
( x in F1 iff x is Functor of C,D ) and
A4: for x being set holds
( x in F2 iff x is Functor of C,D ) ; ::_thesis: F1 = F2
now__::_thesis:_for_x_being_set_holds_
(_x_in_F1_iff_x_in_F2_)
let x be set ; ::_thesis: ( x in F1 iff x in F2 )
 ( x in F1 iff x is Functor of C,D ) by A3;
hence  ( x in F1 iff x in F2 ) by A4; ::_thesis: verum
end;
hence  F1 = F2 by TARSKI:1; ::_thesis: verum
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
set x = the Functor of C,D;
 the Functor of C,D in Funct (C,D) by Def2;
hence  not Funct (C,D) is empty ; ::_thesis: verum
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
take  Funct (C,D) ; ::_thesis: for x being Element of Funct (C,D) holds x is Functor of C,D
thus  for x being Element of Funct (C,D) holds x is Functor of C,D by Def2; ::_thesis: verum
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 funcT . x ->  Element of F;
coherence
 T . x is Element of F
proof
thus  T . x is Element of F ; ::_thesis: verum
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
let x be Element of Funct (C,D); :: according to CAT_2:def_3 ::_thesis: x is Functor of C,D
thus  x is Functor of C,D by Def2; ::_thesis: verum
end;
end;

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

:: deftheorem Def4 defines Subcategory CAT_2:def_4_:_
 for C, b2 being Category holds
( b2 is Subcategory of C iff ( the carrier of b2 c= the carrier of C & ( for a, b being Object of b2
for a9, b9 being Object of C st a = a9 & b = b9 holds
Hom (a,b) c= Hom (a9,b9) ) & the Comp of b2 c= the Comp of C & ( for a being Object of b2
for a9 being Object of C st a = a9 holds
id a = id a9 ) ) );

registration
let C be Category;
cluster non empty non void V55() strict Category-like transitive associative reflexive with_identities for Subcategory of C;
existence
 ex b1 being Subcategory of C st b1 is strict
proof
set c = the Object of C;
set E = 1Cat ( the Object of C,(id the Object of C));
now__::_thesis:_(_the_carrier_of_(1Cat_(_the_Object_of_C,(id_the_Object_of_C)))_c=_the_carrier_of_C_&_(_for_a,_b_being_Object_of_(1Cat_(_the_Object_of_C,(id_the_Object_of_C)))
for_a9,_b9_being_Object_of_C_st_a_=_a9_&_b_=_b9_holds_
Hom_(a,b)_c=_Hom_(a9,b9)_)_&_the_Comp_of_(1Cat_(_the_Object_of_C,(id_the_Object_of_C)))_c=_the_Comp_of_C_&_(_for_a_being_Object_of_(1Cat_(_the_Object_of_C,(id_the_Object_of_C)))
for_a9_being_Object_of_C_st_a_=_a9_holds_
id_a_=_id_a9_)_)
thus  the carrier of (1Cat ( the Object of C,(id the Object of C))) c= the carrier of C ::_thesis: ( ( for a, b being Object of (1Cat ( the Object of C,(id the Object of C)))
for a9, b9 being Object of C st a = a9 & b = b9 holds
Hom (a,b) c= Hom (a9,b9) ) & the Comp of (1Cat ( the Object of C,(id the Object of C))) c= the Comp of C & ( for a being Object of (1Cat ( the Object of C,(id the Object of C)))
for a9 being Object of C st a = a9 holds
id a = id a9 ) )
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in the carrier of (1Cat ( the Object of C,(id the Object of C))) or a in the carrier of C )
assume  a in the carrier of (1Cat ( the Object of C,(id the Object of C))) ; ::_thesis: a in the carrier of C
then  a = the Object of C by TARSKI:def_1;
hence  a in the carrier of C ; ::_thesis: verum
end;
thus  for a, b being Object of (1Cat ( the Object of C,(id the Object of C)))
for a9, b9 being Object of C st a = a9 & b = b9 holds
Hom (a,b) c= Hom (a9,b9) ::_thesis: ( the Comp of (1Cat ( the Object of C,(id the Object of C))) c= the Comp of C & ( for a being Object of (1Cat ( the Object of C,(id the Object of C)))
for a9 being Object of C st a = a9 holds
id a = id a9 ) )
proof
let a, b be Object of (1Cat ( the Object of C,(id the Object of C))); ::_thesis: for a9, b9 being Object of C st a = a9 & b = b9 holds
Hom (a,b) c= Hom (a9,b9)
let a9, b9 be Object of C; ::_thesis: ( a = a9 & b = b9 implies Hom (a,b) c= Hom (a9,b9) )
assume  ( a = a9 & b = b9 ) ; ::_thesis: Hom (a,b) c= Hom (a9,b9)
then A1: ( a9 = the Object of C & b9 = the Object of C ) by TARSKI:def_1;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Hom (a,b) or x in Hom (a9,b9) )
assume  x in Hom (a,b) ; ::_thesis: x in Hom (a9,b9)
then  x = id the Object of C by TARSKI:def_1;
hence  x in Hom (a9,b9) by A1, CAT_1:27; ::_thesis: verum
end;
thus  the Comp of (1Cat ( the Object of C,(id the Object of C))) c= the Comp of C ::_thesis: for a being Object of (1Cat ( the Object of C,(id the Object of C)))
for a9 being Object of C st a = a9 holds
id a = id a9
proof
reconsider i = id the Object of C as Morphism of C ;
A2: Hom ( the Object of C, the Object of C) <> {} ;
A3: ( dom (id the Object of C) = the Object of C & cod (id the Object of C) = the Object of C ) ;
then A4: [(id the Object of C),(id the Object of C)] in dom the Comp of C by CAT_1:15;
the Comp of (1Cat ( the Object of C,(id the Object of C))) = ((id the Object of C),(id the Object of C)) .--> ((id the Object of C) * (id the Object of C))
.= ((id the Object of C),(id the Object of C)) .--> ((id the Object of C) (*) i) by A2, CAT_1:def_13
.= [(id the Object of C),(id the Object of C)] .--> ( the Comp of C . ((id the Object of C),(id the Object of C))) by A3, CAT_1:16 ;
hence  the Comp of (1Cat ( the Object of C,(id the Object of C))) c= the Comp of C by A4, FUNCT_4:7; ::_thesis: verum
end;
let a be Object of (1Cat ( the Object of C,(id the Object of C))); ::_thesis: for a9 being Object of C st a = a9 holds
id a = id a9
let a9 be Object of C; ::_thesis: ( a = a9 implies id a = id a9 )
assume  a = a9 ; ::_thesis: id a = id a9
then  a9 = the Object of C by TARSKI:def_1;
hence  id a = id a9 by TARSKI:def_1; ::_thesis: verum
end;
then  1Cat ( the Object of C,(id the Object of C)) is Subcategory of C by Def4;
hence  ex b1 being Subcategory of C st b1 is strict ; ::_thesis: verum
end;
end;

theorem Th6: :: CAT_2:6
for C being Category
for E being Subcategory of C
for e being Object of E holds e is Object of C
proof
let C be Category; ::_thesis: for E being Subcategory of C
for e being Object of E holds e is Object of C
let E be Subcategory of C; ::_thesis: for e being Object of E holds e is Object of C
let e be Object of E; ::_thesis: e is Object of C
 ( e in the carrier of E & the carrier of E c= the carrier of C ) by Def4;
hence  e is Object of C ; ::_thesis: verum
end;

theorem Th7: :: CAT_2:7
for C being Category
for E being Subcategory of C holds the carrier' of E c= the carrier' of C
proof
let C be Category; ::_thesis: for E being Subcategory of C holds the carrier' of E c= the carrier' of C
let E be Subcategory of C; ::_thesis: the carrier' of E c= the carrier' of C
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier' of E or x in the carrier' of C )
assume  x in the carrier' of E ; ::_thesis: x in the carrier' of C
then reconsider f = x as Morphism of E ;
set a = dom f;
set b = cod f;
reconsider a9 = dom f, b9 = cod f as Object of C by Th6;
 ( f in Hom ((dom f),(cod f)) & Hom ((dom f),(cod f)) c= Hom (a9,b9) ) by Def4;
then  ( f in Hom (a9,b9) & Hom (a9,b9) <> {} ) ;
hence  x in the carrier' of C ; ::_thesis: verum
end;

theorem Th8: :: CAT_2:8
for C being Category
for E being Subcategory of C
for f being Morphism of E holds f is Morphism of C
proof
let C be Category; ::_thesis: for E being Subcategory of C
for f being Morphism of E holds f is Morphism of C
let E be Subcategory of C; ::_thesis: for f being Morphism of E holds f is Morphism of C
let f be Morphism of E; ::_thesis: f is Morphism of C
 ( f in the carrier' of E & the carrier' of E c= the carrier' of C ) by Th7;
hence  f is Morphism of C ; ::_thesis: verum
end;

theorem Th9: :: CAT_2:9
for C being Category
for E being Subcategory of C
for f being Morphism of E
for f9 being Morphism of C st f = f9 holds
( dom f = dom f9 & cod f = cod f9 )
proof
let C be Category; ::_thesis: for E being Subcategory of C
for f being Morphism of E
for f9 being Morphism of C st f = f9 holds
( dom f = dom f9 & cod f = cod f9 )
let E be Subcategory of C; ::_thesis: for f being Morphism of E
for f9 being Morphism of C st f = f9 holds
( dom f = dom f9 & cod f = cod f9 )
let f be Morphism of E; ::_thesis: for f9 being Morphism of C st f = f9 holds
( dom f = dom f9 & cod f = cod f9 )
let f9 be Morphism of C; ::_thesis: ( f = f9 implies ( dom f = dom f9 & cod f = cod f9 ) )
assume A1: f = f9 ; ::_thesis: ( dom f = dom f9 & cod f = cod f9 )
set a = dom f;
set b = cod f;
reconsider a9 = dom f, b9 = cod f as Object of C by Th6;
 ( f in Hom ((dom f),(cod f)) & Hom ((dom f),(cod f)) c= Hom (a9,b9) ) by Def4;
hence  ( dom f = dom f9 & cod f = cod f9 ) by A1, CAT_1:1; ::_thesis: verum
end;

theorem :: CAT_2:10
for C being Category
for E being Subcategory of C
for a, b being Object of E
for a9, b9 being Object of C
for f being Morphism of a,b st a = a9 & b = b9 & Hom (a,b) <> {} holds
f is Morphism of a9,b9
proof
let C be Category; ::_thesis: for E being Subcategory of C
for a, b being Object of E
for a9, b9 being Object of C
for f being Morphism of a,b st a = a9 & b = b9 & Hom (a,b) <> {} holds
f is Morphism of a9,b9
let E be Subcategory of C; ::_thesis: for a, b being Object of E
for a9, b9 being Object of C
for f being Morphism of a,b st a = a9 & b = b9 & Hom (a,b) <> {} holds
f is Morphism of a9,b9
let a, b be Object of E; ::_thesis: for a9, b9 being Object of C
for f being Morphism of a,b st a = a9 & b = b9 & Hom (a,b) <> {} holds
f is Morphism of a9,b9
let a9, b9 be Object of C; ::_thesis: for f being Morphism of a,b st a = a9 & b = b9 & Hom (a,b) <> {} holds
f is Morphism of a9,b9
let f be Morphism of a,b; ::_thesis: ( a = a9 & b = b9 & Hom (a,b) <> {} implies f is Morphism of a9,b9 )
assume  ( a = a9 & b = b9 & Hom (a,b) <> {} ) ; ::_thesis: f is Morphism of a9,b9
then  ( f in Hom (a,b) & Hom (a,b) c= Hom (a9,b9) ) by Def4, CAT_1:def_5;
then  ( f in Hom (a9,b9) & Hom (a9,b9) <> {} ) ;
hence  f is Morphism of a9,b9 by CAT_1:def_5; ::_thesis: verum
end;

theorem Th11: :: CAT_2:11
for C being Category
for E being Subcategory of C
for f, g being Morphism of E
for f9, g9 being Morphism of C st f = f9 & g = g9 & dom g = cod f holds
g (*) f = g9 (*) f9
proof
let C be Category; ::_thesis: for E being Subcategory of C
for f, g being Morphism of E
for f9, g9 being Morphism of C st f = f9 & g = g9 & dom g = cod f holds
g (*) f = g9 (*) f9
let E be Subcategory of C; ::_thesis: for f, g being Morphism of E
for f9, g9 being Morphism of C st f = f9 & g = g9 & dom g = cod f holds
g (*) f = g9 (*) f9
let f, g be Morphism of E; ::_thesis: for f9, g9 being Morphism of C st f = f9 & g = g9 & dom g = cod f holds
g (*) f = g9 (*) f9
let f9, g9 be Morphism of C; ::_thesis: ( f = f9 & g = g9 & dom g = cod f implies g (*) f = g9 (*) f9 )
assume that
A1: ( f = f9 & g = g9 ) and
A2: dom g = cod f ; ::_thesis: g (*) f = g9 (*) f9
 ( dom g = dom g9 & cod f = cod f9 ) by A1, Th9;
then A3: g9 (*) f9 = the Comp of C . (g9,f9) by A2, CAT_1:16;
A4: the Comp of E c= the Comp of C by Def4;
 ( g (*) f = the Comp of E . (g,f) & [g,f] in dom the Comp of E ) by A2, CAT_1:15, CAT_1:16;
hence  g (*) f = g9 (*) f9 by A1, A3, A4, GRFUNC_1:2; ::_thesis: verum
end;

theorem Th12: :: CAT_2:12
for C being Category holds C is Subcategory of C
proof
let C be Category; ::_thesis: C is Subcategory of C
thus  the carrier of C c= the carrier of C ; :: according to CAT_2:def_4 ::_thesis: ( ( for a, b, a9, b9 being Object of C st a = a9 & b = b9 holds
Hom (a,b) c= Hom (a9,b9) ) & the Comp of C c= the Comp of C & ( for a, a9 being Object of C st a = a9 holds
id a = id a9 ) )
thus  ( ( for a, b, a9, b9 being Object of C st a = a9 & b = b9 holds
Hom (a,b) c= Hom (a9,b9) ) & the Comp of C c= the Comp of C & ( for a, a9 being Object of C st a = a9 holds
id a = id a9 ) ) ; ::_thesis: verum
end;

theorem Th13: :: CAT_2:13
for C being Category
for E being Subcategory of C holds id E is Functor of E,C
proof
let C be Category; ::_thesis: for E being Subcategory of C holds id E is Functor of E,C
let E be Subcategory of C; ::_thesis: id E is Functor of E,C
 rng (id E) = the carrier' of E by RELAT_1:45;
then  rng (id E) c= the carrier' of C by Th7;
then reconsider T = id E as Function of the carrier' of E, the carrier' of C by FUNCT_2:6;
now__::_thesis:_(_(_for_e_being_Object_of_E_ex_c_being_Object_of_C_st_T_._(id_e)_=_id_c_)_&_(_for_f_being_Morphism_of_E_holds_
(_T_._(id_(dom_f))_=_id_(dom_(T_._f))_&_T_._(id_(cod_f))_=_id_(cod_(T_._f))_)_)_&_(_for_f,_g_being_Morphism_of_E_st_dom_g_=_cod_f_holds_
T_._(g_(*)_f)_=_(T_._g)_(*)_(T_._f)_)_)
thus  for e being Object of E ex c being Object of C st T . (id e) = id c ::_thesis: ( ( for f being Morphism of E holds
( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) ) ) & ( for f, g being Morphism of E st dom g = cod f holds
T . (g (*) f) = (T . g) (*) (T . f) ) )
proof
let e be Object of E; ::_thesis: ex c being Object of C st T . (id e) = id c
reconsider c = e as Object of C by Th6;
T . (id e) = id e by FUNCT_1:18
.= id c by Def4 ;
hence  ex c being Object of C st T . (id e) = id c ; ::_thesis: verum
end;
thus  for f being Morphism of E holds
( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) ) ::_thesis: for f, g being Morphism of E st dom g = cod f holds
T . (g (*) f) = (T . g) (*) (T . f)
proof
let f be Morphism of E; ::_thesis: ( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) )
A1: T . (id (dom f)) = id (dom f) by FUNCT_1:18
.= id (dom ((id E) . f)) by FUNCT_1:18 ;
A2: T . (id (cod f)) = id (cod f) by FUNCT_1:18
.= id (cod ((id E) . f)) by FUNCT_1:18 ;
 ( dom (T . f) = dom ((id E) . f) & cod (T . f) = cod ((id E) . f) ) by Th9;
hence  ( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) ) by A1, A2, Def4; ::_thesis: verum
end;
let f, g be Morphism of E; ::_thesis: ( dom g = cod f implies T . (g (*) f) = (T . g) (*) (T . f) )
A3: ( T . f = f & T . g = g ) by FUNCT_1:18;
assume A4: dom g = cod f ; ::_thesis: T . (g (*) f) = (T . g) (*) (T . f)
then  T . (g (*) f) = ((id E) . g) (*) ((id E) . f) by CAT_1:64;
hence  T . (g (*) f) = (T . g) (*) (T . f) by A4, A3, Th11; ::_thesis: verum
end;
hence  id E is Functor of E,C by CAT_1:61; ::_thesis: verum
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 Th13;
end;

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

theorem Th14: :: CAT_2:14
for C being Category
for E being Subcategory of C
for a being Object of E holds (Obj (incl E)) . a = a
proof
let C be Category; ::_thesis: for E being Subcategory of C
for a being Object of E holds (Obj (incl E)) . a = a
let E be Subcategory of C; ::_thesis: for a being Object of E holds (Obj (incl E)) . a = a
let a be Object of E; ::_thesis: (Obj (incl E)) . a = a
reconsider a9 = a as Object of C by Th6;
id a9 = id a by Def4
.= (incl E) . (id a) by FUNCT_1:18
.= id ((Obj (incl E)) . a) by CAT_1:68 ;
hence  (Obj (incl E)) . a = a by CAT_1:59; ::_thesis: verum
end;

theorem :: CAT_2:15
for C being Category
for E being Subcategory of C
for a being Object of E holds (incl E) . a = a by Th14;

theorem :: CAT_2:16
for C being Category
for E being Subcategory of C holds incl E is faithful
proof
let C be Category; ::_thesis: for E being Subcategory of C holds incl E is faithful
let E be Subcategory of C; ::_thesis: incl E is faithful
let a, b be Object of E; :: according to CAT_1:def_27 ::_thesis: ( Hom (a,b) = {} or for b1, b2 being Morphism of a,b holds
( not (incl E) . b1 = (incl E) . b2 or b1 = b2 ) )
assume  Hom (a,b) <> {} ; ::_thesis: for b1, b2 being Morphism of a,b holds
( not (incl E) . b1 = (incl E) . b2 or b1 = b2 )
let f1, f2 be Morphism of a,b; ::_thesis: ( not (incl E) . f1 = (incl E) . f2 or f1 = f2 )
 (incl E) . f1 = f1 by FUNCT_1:18;
hence  ( not (incl E) . f1 = (incl E) . f2 or f1 = f2 ) by FUNCT_1:18; ::_thesis: verum
end;

theorem Th17: :: CAT_2:17
for C being Category
for E being Subcategory of C holds
( incl E is full iff for a, b being Object of E
for a9, b9 being Object of C st a = a9 & b = b9 holds
Hom (a,b) = Hom (a9,b9) )
proof
let C be Category; ::_thesis: for E being Subcategory of C holds
( incl E is full iff for a, b being Object of E
for a9, b9 being Object of C st a = a9 & b = b9 holds
Hom (a,b) = Hom (a9,b9) )
let E be Subcategory of C; ::_thesis: ( incl E is full iff for a, b being Object of E
for a9, b9 being Object of C st a = a9 & b = b9 holds
Hom (a,b) = Hom (a9,b9) )
set T = incl E;
thus  ( incl E is full implies for a, b being Object of E
for a9, b9 being Object of C st a = a9 & b = b9 holds
Hom (a,b) = Hom (a9,b9) ) ::_thesis: ( ( for a, b being Object of E
for a9, b9 being Object of C st a = a9 & b = b9 holds
Hom (a,b) = Hom (a9,b9) ) implies incl E is full )
proof
assume A1: for a, b being Object of E st Hom (((incl E) . a),((incl E) . b)) <> {} holds
for g being Morphism of (incl E) . a,(incl E) . b holds
( Hom (a,b) <> {} & ex f being Morphism of a,b st g = (incl E) . f ) ; :: according to CAT_1:def_26 ::_thesis: for a, b being Object of E
for a9, b9 being Object of C st a = a9 & b = b9 holds
Hom (a,b) = Hom (a9,b9)
let a, b be Object of E; ::_thesis: for a9, b9 being Object of C st a = a9 & b = b9 holds
Hom (a,b) = Hom (a9,b9)
let a9, b9 be Object of C; ::_thesis: ( a = a9 & b = b9 implies Hom (a,b) = Hom (a9,b9) )
assume A2: ( a = a9 & b = b9 ) ; ::_thesis: Hom (a,b) = Hom (a9,b9)
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_Hom_(a,b)_implies_x_in_Hom_(a9,b9)_)_&_(_x_in_Hom_(a9,b9)_implies_x_in_Hom_(a,b)_)_)
let x be set ; ::_thesis: ( ( x in Hom (a,b) implies x in Hom (a9,b9) ) & ( x in Hom (a9,b9) implies x in Hom (a,b) ) )
 Hom (a,b) c= Hom (a9,b9) by A2, Def4;
hence  ( x in Hom (a,b) implies x in Hom (a9,b9) ) ; ::_thesis: ( x in Hom (a9,b9) implies x in Hom (a,b) )
assume A3: x in Hom (a9,b9) ; ::_thesis: x in Hom (a,b)
A4: ( (incl E) . a = a9 & (incl E) . b = b9 ) by A2, Th14;
then reconsider g = x as Morphism of (incl E) . a,(incl E) . b by A3, CAT_1:def_5;
consider f being Morphism of a,b such that
A5: g = (incl E) . f by A1, A4, A3;
A6: g = f by A5, FUNCT_1:18;
 Hom (a,b) <> {} by A1, A4, A3;
hence  x in Hom (a,b) by A6, CAT_1:def_5; ::_thesis: verum
end;
hence  Hom (a,b) = Hom (a9,b9) by TARSKI:1; ::_thesis: verum
end;
assume A7: for a, b being Object of E
for a9, b9 being Object of C st a = a9 & b = b9 holds
Hom (a,b) = Hom (a9,b9) ; ::_thesis: incl E is full
let a, b be Object of E; :: according to CAT_1:def_26 ::_thesis: ( Hom (((incl E) . a),((incl E) . b)) = {} or for b1 being Morphism of (incl E) . a,(incl E) . b holds
( not Hom (a,b) = {} & ex b2 being Morphism of a,b st b1 = (incl E) . b2 ) )
assume A8: Hom (((incl E) . a),((incl E) . b)) <> {} ; ::_thesis: for b1 being Morphism of (incl E) . a,(incl E) . b holds
( not Hom (a,b) = {} & ex b2 being Morphism of a,b st b1 = (incl E) . b2 )
let g be Morphism of (incl E) . a,(incl E) . b; ::_thesis: ( not Hom (a,b) = {} & ex b1 being Morphism of a,b st g = (incl E) . b1 )
A9: g in Hom (((incl E) . a),((incl E) . b)) by A8, CAT_1:def_5;
A10: ( a = (incl E) . a & b = (incl E) . b ) by Th14;
hence  Hom (a,b) <> {} by A7, A8; ::_thesis: ex b1 being Morphism of a,b st g = (incl E) . b1
 Hom (a,b) = Hom (((incl E) . a),((incl E) . b)) by A7, A10;
then reconsider f = g as Morphism of a,b by A9, CAT_1:def_5;
take  f ; ::_thesis: g = (incl E) . f
thus  g = (incl E) . f by FUNCT_1:18; ::_thesis: verum
end;

definition
let D be Category;
let C be Subcategory of D;
attrC is full  means :Def6: :: CAT_2:def 6
 for c1, c2 being Object of C
for d1, d2 being Object of D st c1 = d1 & c2 = d2 holds
Hom (c1,c2) = Hom (d1,d2);
end;

:: deftheorem Def6 defines full CAT_2:def_6_:_
 for D being Category
for C being Subcategory of D holds
( C is full iff for c1, c2 being Object of C
for d1, d2 being Object of D st c1 = d1 & c2 = d2 holds
Hom (c1,c2) = Hom (d1,d2) );

registration
let D be Category;
cluster non empty non void V55() Category-like transitive associative reflexive with_identities full for Subcategory of D;
existence
 ex b1 being Subcategory of D st b1 is full
proof
reconsider C = D as Subcategory of D by Th12;
take  C ; ::_thesis: C is full
let c1, c2 be Object of C; :: according to CAT_2:def_6 ::_thesis: for d1, d2 being Object of D st c1 = d1 & c2 = d2 holds
Hom (c1,c2) = Hom (d1,d2)
let d1, d2 be Object of D; ::_thesis: ( c1 = d1 & c2 = d2 implies Hom (c1,c2) = Hom (d1,d2) )
assume  ( c1 = d1 & c2 = d2 ) ; ::_thesis: Hom (c1,c2) = Hom (d1,d2)
hence  Hom (c1,c2) = Hom (d1,d2) ; ::_thesis: verum
end;
end;

theorem :: CAT_2:18
for C being Category
for E being Subcategory of C holds
( E is full iff incl E is full )
proof
let C be Category; ::_thesis: for E being Subcategory of C holds
( E is full iff incl E is full )
let E be Subcategory of C; ::_thesis: ( E is full iff incl E is full )
thus  ( E is full implies incl E is full ) ::_thesis: ( incl E is full implies E is full )
proof
assume  E is full ; ::_thesis: incl E is full
then  for a, b being Object of E
for a9, b9 being Object of C st a = a9 & b = b9 holds
Hom (a,b) = Hom (a9,b9) by Def6;
hence  incl E is full by Th17; ::_thesis: verum
end;
assume  incl E is full ; ::_thesis: E is full
hence  for a, b being Object of E
for a9, b9 being Object of C st a = a9 & b = b9 holds
Hom (a,b) = Hom (a9,b9) by Th17; :: according to CAT_2:def_6 ::_thesis: verum
end;

theorem Th19: :: CAT_2:19
for C being Category
for O being non empty Subset of the carrier 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 carrier' of C
proof
let C be Category; ::_thesis: for O being non empty Subset of the carrier 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 carrier' of C
let O be non empty Subset of the carrier of C; ::_thesis: union  {  (Hom (a,b)) where a, b is Object of C : ( a in O & b in O )  }  is non empty Subset of the carrier' of C
set H =  {  (Hom (a,b)) where a, b is Object of C : ( a in O & b in O )  }  ;
set M = union  {  (Hom (a,b)) where a, b is Object of C : ( a in O & b in O )  }  ;
A1: union  {  (Hom (a,b)) where a, b is Object of C : ( a in O & b in O )  }  c= the carrier' of C
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union  {  (Hom (a,b)) where a, b is Object of C : ( a in O & b in O )  }  or x in the carrier' of C )
assume  x in union  {  (Hom (a,b)) where a, b is Object of C : ( a in O & b in O )  }  ; ::_thesis: x in the carrier' of C
then consider X being set  such that
A2: x in X and
A3: X in  {  (Hom (a,b)) where a, b is Object of C : ( a in O & b in O )  }  by TARSKI:def_4;
 ex a, b being Object of C st
( X = Hom (a,b) & a in O & b in O ) by A3;
hence  x in the carrier' of C by A2; ::_thesis: verum
end;
now__::_thesis:_ex_f_being_set_st_f_in_union__{__(Hom_(a,b))_where_a,_b_is_Object_of_C_:_(_a_in_O_&_b_in_O_)__}_
set a = the Element of O;
reconsider a = the Element of O as Object of C ;
 ( id a in Hom (a,a) & Hom (a,a) in  {  (Hom (a,b)) where a, b is Object of C : ( a in O & b in O )  }  ) by CAT_1:27;
then  id a in union  {  (Hom (a,b)) where a, b is Object of C : ( a in O & b in O )  }  by TARSKI:def_4;
hence  ex f being set st f in union  {  (Hom (a,b)) where a, b is Object of C : ( a in O & b in O )  }  ; ::_thesis: verum
end;
hence  union  {  (Hom (a,b)) where a, b is Object of C : ( a in O & b in O )  }  is non empty Subset of the carrier' of C by A1; ::_thesis: verum
end;

theorem Th20: :: CAT_2:20
for C being Category
for O being non empty Subset of the carrier 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 Source of C | M is Function of M,O & the Target of C | M is Function of M,O & the Comp of C || M is PartFunc of [:M,M:],M )
proof
let C be Category; ::_thesis: for O being non empty Subset of the carrier 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 Source of C | M is Function of M,O & the Target of C | M is Function of M,O & the Comp of C || M is PartFunc of [:M,M:],M )
let O be non empty Subset of the carrier of C; ::_thesis: 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 Source of C | M is Function of M,O & the Target of C | M is Function of M,O & the Comp of C || M is PartFunc of [:M,M:],M )
set H =  {  (Hom (a,b)) where a, b is Object of C : ( a in O & b in O )  }  ;
A1: dom the Source of C = the carrier' of C by FUNCT_2:def_1;
let M be non empty set ; ::_thesis: ( M = union  {  (Hom (a,b)) where a, b is Object of C : ( a in O & b in O )  }  implies ( the Source of C | M is Function of M,O & the Target of C | M is Function of M,O & the Comp of C || M is PartFunc of [:M,M:],M ) )
assume A2: M = union  {  (Hom (a,b)) where a, b is Object of C : ( a in O & b in O )  }  ; ::_thesis: ( the Source of C | M is Function of M,O & the Target of C | M is Function of M,O & the Comp of C || M is PartFunc of [:M,M:],M )
A3: now__::_thesis:_for_f_being_Morphism_of_C_st_f_in_M_holds_
(_dom_f_in_O_&_cod_f_in_O_)
let f be Morphism of C; ::_thesis: ( f in M implies ( dom f in O & cod f in O ) )
assume  f in M ; ::_thesis: ( dom f in O & cod f in O )
then consider X being set  such that
A4: f in X and
A5: X in  {  (Hom (a,b)) where a, b is Object of C : ( a in O & b in O )  }  by A2, TARSKI:def_4;
 ex a, b being Object of C st
( X = Hom (a,b) & a in O & b in O ) by A5;
hence  ( dom f in O & cod f in O ) by A4, CAT_1:1; ::_thesis: verum
end;
set d = the Source of C | M;
set c = the Target of C | M;
set p = the Comp of C || M;
A6: dom the Target of C = the carrier' of C by FUNCT_2:def_1;
A7: dom ( the Source of C | M) = (dom the Source of C) /\ M by RELAT_1:61;
A8: rng ( the Source of C | M) c= O
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng ( the Source of C | M) or y in O )
assume  y in rng ( the Source of C | M) ; ::_thesis: y in O
then consider x being set  such that
A9: x in dom ( the Source of C | M) and
A10: y = ( the Source of C | M) . x by FUNCT_1:def_3;
reconsider f = x as Morphism of C by A1, A7, A9, XBOOLE_0:def_4;
 ( ( the Source of C | M) . f = dom f & f in M ) by A7, A9, FUNCT_1:47, XBOOLE_0:def_4;
hence  y in O by A3, A10; ::_thesis: verum
end;
A11: M is non empty Subset of the carrier' of C by A2, Th19;
then A12: dom ( the Target of C | M) = M by A6, RELAT_1:62;
A13: dom ( the Target of C | M) = (dom the Target of C) /\ M by RELAT_1:61;
A14: rng ( the Target of C | M) c= O
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng ( the Target of C | M) or y in O )
assume  y in rng ( the Target of C | M) ; ::_thesis: y in O
then consider x being set  such that
A15: x in dom ( the Target of C | M) and
A16: y = ( the Target of C | M) . x by FUNCT_1:def_3;
reconsider f = x as Morphism of C by A6, A13, A15, XBOOLE_0:def_4;
 ( ( the Target of C | M) . f = cod f & f in M ) by A13, A15, FUNCT_1:47, XBOOLE_0:def_4;
hence  y in O by A3, A16; ::_thesis: verum
end;
 dom ( the Source of C | M) = M by A1, A11, RELAT_1:62;
hence  ( the Source of C | M is Function of M,O & the Target of C | M is Function of M,O ) by A8, A14, A12, FUNCT_2:def_1, RELSET_1:4; ::_thesis: the Comp of C || M is PartFunc of [:M,M:],M
A17: dom ( the Comp of C || M) = (dom the Comp of C) /\ [:M,M:] by RELAT_1:61;
A18: dom the Comp of C c= [: the carrier' of C, the carrier' of C:] by RELAT_1:def_18;
 rng ( the Comp of C || M) c= M
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng ( the Comp of C || M) or y in M )
assume  y in rng ( the Comp of C || M) ; ::_thesis: y in M
then consider x being set  such that
A19: x in dom ( the Comp of C || M) and
A20: y = ( the Comp of C || M) . x by FUNCT_1:def_3;
A21: x in dom the Comp of C by A17, A19, XBOOLE_0:def_4;
then consider g, f being Morphism of C such that
A22: x = [g,f] by A18, DOMAIN_1:1;
A23: [g,f] in [:M,M:] by A17, A19, A22, XBOOLE_0:def_4;
then  g in M by ZFMISC_1:87;
then A24: cod g in O by A3;
 dom g = cod f by A21, A22, CAT_1:15;
then A25: ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) by CAT_1:17;
 f in M by A23, ZFMISC_1:87;
then  dom f in O by A3;
then A26: Hom ((dom (g (*) f)),(cod (g (*) f))) in  {  (Hom (a,b)) where a, b is Object of C : ( a in O & b in O )  }  by A24, A25;
A27: g (*) f in Hom ((dom (g (*) f)),(cod (g (*) f))) ;
( the Comp of C || M) . x = the Comp of C . (g,f) by A19, A22, FUNCT_1:47
.= g (*) f by A21, A22, CAT_1:def_1 ;
hence  y in M by A2, A20, A26, A27, TARSKI:def_4; ::_thesis: verum
end;
hence  the Comp of C || M is PartFunc of [:M,M:],M by A17, RELSET_1:4, XBOOLE_1:17; ::_thesis: verum
thus  verum ; ::_thesis: verum
end;

registration
let O, M be non empty set ;
let d, c be Function of M,O;
let p be PartFunc of [:M,M:],M;
cluster CatStr(# O,M,d,c,p #) ->  non empty non void ;
coherence
 ( not CatStr(# O,M,d,c,p #) is void & not CatStr(# O,M,d,c,p #) is empty ) ;
end;

Lm1:  for C being Category
for O being non empty Subset of the carrier 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 Source of C | M & c = the Target of C | M & p = the Comp of C || M holds
CatStr(# O,M,d,c,p #) is Category
proof
let C be Category; ::_thesis: for O being non empty Subset of the carrier 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 Source of C | M & c = the Target of C | M & p = the Comp of C || M holds
CatStr(# O,M,d,c,p #) is Category
let O be non empty Subset of the carrier of C; ::_thesis: 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 Source of C | M & c = the Target of C | M & p = the Comp of C || M holds
CatStr(# O,M,d,c,p #) is Category
let M be non empty set ; ::_thesis: 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 Source of C | M & c = the Target of C | M & p = the Comp of C || M holds
CatStr(# O,M,d,c,p #) is Category
let d, c be Function of M,O; ::_thesis: 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 Source of C | M & c = the Target of C | M & p = the Comp of C || M holds
CatStr(# O,M,d,c,p #) is Category
let p be PartFunc of [:M,M:],M; ::_thesis: 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 Source of C | M & c = the Target of C | M & p = the Comp of C || M holds
CatStr(# O,M,d,c,p #) is Category
let i be Function of O,M; ::_thesis: ( M = union  {  (Hom (a,b)) where a, b is Object of C : ( a in O & b in O )  }  & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M implies CatStr(# O,M,d,c,p #) is Category )
set H =  {  (Hom (a,b)) where a, b is Object of C : ( a in O & b in O )  }  ;
assume that
A1: M = union  {  (Hom (a,b)) where a, b is Object of C : ( a in O & b in O )  }  and
A2: d = the Source of C | M and
A3: c = the Target of C | M and
A4: p = the Comp of C || M ; ::_thesis: CatStr(# O,M,d,c,p #) is Category
set B = CatStr(# O,M,d,c,p #);
A5: now__::_thesis:_for_f_being_Morphism_of_CatStr(#_O,M,d,c,p_#)_holds_f_is_Morphism_of_C
let f be Morphism of CatStr(# O,M,d,c,p #); ::_thesis: f is Morphism of C
consider X being set  such that
A6: f in X and
A7: X in  {  (Hom (a,b)) where a, b is Object of C : ( a in O & b in O )  }  by A1, TARSKI:def_4;
 ex a, b being Object of C st
( X = Hom (a,b) & a in O & b in O ) by A7;
hence  f is Morphism of C by A6; ::_thesis: verum
end;
A8: for f, g being Morphism of CatStr(# O,M,d,c,p #) holds
( [g,f] in dom p iff d . g = c . f )
proof
let f, g be Morphism of CatStr(# O,M,d,c,p #); ::_thesis: ( [g,f] in dom p iff d . g = c . f )
reconsider gg = g, ff = f as Morphism of C by A5;
A9: ( d . g = dom gg & c . f = cod ff ) by A2, A3, FUNCT_1:49;
thus  ( [g,f] in dom p implies d . g = c . f ) ::_thesis: ( d . g = c . f implies [g,f] in dom p )
proof
assume  [g,f] in dom p ; ::_thesis: d . g = c . f
then  [g,f] in (dom the Comp of C) /\ [:M,M:] by A4, RELAT_1:61;
then  [gg,ff] in dom the Comp of C by XBOOLE_0:def_4;
hence  d . g = c . f by A9, CAT_1:def_6; ::_thesis: verum
end;
assume  d . g = c . f ; ::_thesis: [g,f] in dom p
then  [g,f] in dom the Comp of C by A9, CAT_1:def_6;
then  [g,f] in (dom the Comp of C) /\ [:M,M:] by XBOOLE_0:def_4;
hence  [g,f] in dom p by A4, RELAT_1:61; ::_thesis: verum
end;
A10: CatStr(# O,M,d,c,p #) is Category-like
proof
thus  for f, g being Morphism of CatStr(# O,M,d,c,p #) holds
( [g,f] in dom the Comp of CatStr(# O,M,d,c,p #) iff dom g = cod f ) by A8; :: according to CAT_1:def_6 ::_thesis: verum
end;
A11: CatStr(# O,M,d,c,p #) is transitive
proof
thus  for f, g being Morphism of CatStr(# O,M,d,c,p #) st dom g = cod f holds
( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) :: according to CAT_1:def_7 ::_thesis: verum
proof
let f, g be Morphism of CatStr(# O,M,d,c,p #); ::_thesis: ( dom g = cod f implies ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) )
reconsider ff = f, gg = g as Morphism of C by A5;
A12: ( d . g = dom gg & c . f = cod ff ) by A2, A3, FUNCT_1:49;
assume A13: dom g = cod f ; ::_thesis: ( dom (g (*) f) = dom f & cod (g (*) f) = cod g )
A14: [g,f] in dom the Comp of CatStr(# O,M,d,c,p #) by A13, A8;
A15: p . (g,f) = g (*) f by A13, A8, CAT_1:def_1;
A16: dom p c= dom the Comp of C by A4, RELAT_1:60;
A17: p . [g,f] = the Comp of C . (g,f) by A4, A8, A13, FUNCT_1:47
.= gg (*) ff by A16, A14, CAT_1:def_1 ;
thus  dom (g (*) f) = dom (gg (*) ff) by A17, A2, A15, FUNCT_1:49
.= dom ff by A13, A12, CAT_1:def_7
.= dom f by A2, FUNCT_1:49 ; ::_thesis: cod (g (*) f) = cod g
thus  cod (g (*) f) = cod (gg (*) ff) by A17, A3, A15, FUNCT_1:49
.= cod gg by A13, A12, CAT_1:def_7
.= cod g by A3, FUNCT_1:49 ; ::_thesis: verum
end;
end;
A18: CatStr(# O,M,d,c,p #) is associative
proof
thus  for f, g, h being Morphism of CatStr(# O,M,d,c,p #) st dom h = cod g & dom g = cod f holds
h (*) (g (*) f) = (h (*) g) (*) f :: according to CAT_1:def_8 ::_thesis: verum
proof
let f, g, h be Morphism of CatStr(# O,M,d,c,p #); ::_thesis: ( dom h = cod g & dom g = cod f implies h (*) (g (*) f) = (h (*) g) (*) f )
reconsider ff = f, gg = g, hh = h as Morphism of C by A5;
assume that
A19: dom h = cod g and
A20: dom g = cod f ; ::_thesis: h (*) (g (*) f) = (h (*) g) (*) f
A21: h (*) g = the Comp of CatStr(# O,M,d,c,p #) . (h,g) by A19, A8, CAT_1:def_1;
A22: g (*) f = the Comp of CatStr(# O,M,d,c,p #) . (g,f) by A20, A8, CAT_1:def_1;
A23: dom (h (*) g) = dom g by A11, A19, CAT_1:def_7;
A24: ( c . g = cod gg & d . g = dom gg ) by A2, A3, FUNCT_1:49;
A25: c . f = cod ff by A3, FUNCT_1:49;
A26: ( f is Morphism of C & d . h = dom hh ) by A2, A5, FUNCT_1:49;
A27: dom gg = d . g by A2, FUNCT_1:49
.= cod ff by A3, A20, FUNCT_1:49 ;
then A28: gg (*) ff = the Comp of C . (gg,ff) by CAT_1:16;
A29: dom hh = d . h by A2, FUNCT_1:49
.= cod gg by A3, A19, FUNCT_1:49 ;
then A30: cod (gg (*) ff) = dom hh by A27, CAT_1:def_7;
A31: hh (*) gg = the Comp of C . (hh,gg) by A29, CAT_1:16;
A32: cod ff = dom (hh (*) gg) by A27, A29, CAT_1:def_7;
A33: cod (g (*) f) = cod g by A11, A20, CAT_1:def_7;
hence h (*) (g (*) f) = the Comp of CatStr(# O,M,d,c,p #) . (h,( the Comp of CatStr(# O,M,d,c,p #) . (g,f))) by A22, A19, A8, CAT_1:def_1
.= the Comp of C . [h,(p . [g,f])] by A4, A8, A19, A33, A22, FUNCT_1:47
.= the Comp of C . (hh,(gg (*) ff)) by A4, A8, A20, A28, FUNCT_1:47
.= hh (*) (gg (*) ff) by A30, CAT_1:16
.= (hh (*) gg) (*) ff by A19, A20, A26, A24, A25, CAT_1:def_8
.= the Comp of C . (( the Comp of C . (hh,gg)),ff) by A31, A32, CAT_1:16
.= the Comp of C . [(p . [h,g]),f] by A4, A8, A19, FUNCT_1:47
.= the Comp of CatStr(# O,M,d,c,p #) . (( the Comp of CatStr(# O,M,d,c,p #) . (h,g)),f) by A4, A8, A20, A23, A21, FUNCT_1:47
.= (h (*) g) (*) f by A21, A20, A8, A23, CAT_1:def_1 ;
::_thesis: verum
end;
end;
A34: CatStr(# O,M,d,c,p #) is reflexive
proof
let b be Object of CatStr(# O,M,d,c,p #); :: according to CAT_1:def_9 ::_thesis: not Hom (b,b) = {}
 b in O ;
then reconsider bb = b as Object of C ;
A35: Hom (bb,bb) in  {  (Hom (a,b)) where a, b is Object of C : ( a in O & b in O )  }  ;
 id bb in Hom (bb,bb) by CAT_1:27;
then reconsider ii = id bb as Morphism of CatStr(# O,M,d,c,p #) by A35, TARSKI:def_4, A1;
A36: dom ii = dom (id bb) by A2, FUNCT_1:49
.= bb ;
cod ii = cod (id bb) by A3, FUNCT_1:49
.= bb ;
then  ii in Hom (b,b) by A36;
hence  Hom (b,b) <> {} ; ::_thesis: verum
end;
 CatStr(# O,M,d,c,p #) is with_identities
proof
let a be Element of CatStr(# O,M,d,c,p #); :: according to CAT_1:def_10 ::_thesis: ex b1 being Morphism of a,a st
for b2 being Element of the carrier of CatStr(# O,M,d,c,p #) holds
( ( Hom (a,b2) = {} or for b3 being Morphism of a,b2 holds b3 (*) b1 = b3 ) & ( Hom (b2,a) = {} or for b3 being Morphism of b2,a holds b1 (*) b3 = b3 ) )
 a in O ;
then reconsider aa = a as Object of C ;
A37: Hom (aa,aa) in  {  (Hom (a,b)) where a, b is Object of C : ( a in O & b in O )  }  ;
 id aa in Hom (aa,aa) by CAT_1:27;
then reconsider ii = id aa as Morphism of CatStr(# O,M,d,c,p #) by A37, TARSKI:def_4, A1;
A38: dom ii = dom (id aa) by A2, FUNCT_1:49
.= aa ;
A39: cod ii = cod (id aa) by A3, FUNCT_1:49
.= aa ;
then reconsider ii = ii as Morphism of a,a by A38, CAT_1:4;
take  ii ; ::_thesis: for b1 being Element of the carrier of CatStr(# O,M,d,c,p #) holds
( ( Hom (a,b1) = {} or for b2 being Morphism of a,b1 holds b2 (*) ii = b2 ) & ( Hom (b1,a) = {} or for b2 being Morphism of b1,a holds ii (*) b2 = b2 ) )
let b be Element of CatStr(# O,M,d,c,p #); ::_thesis: ( ( Hom (a,b) = {} or for b1 being Morphism of a,b holds b1 (*) ii = b1 ) & ( Hom (b,a) = {} or for b1 being Morphism of b,a holds ii (*) b1 = b1 ) )
 b in O ;
then reconsider bb = b as Object of C ;
thus  ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) ii = g ) ::_thesis: ( Hom (b,a) = {} or for b1 being Morphism of b,a holds ii (*) b1 = b1 )
proof
assume A40: Hom (a,b) <> {} ; ::_thesis: for g being Morphism of a,b holds g (*) ii = g
let g be Morphism of a,b; ::_thesis: g (*) ii = g
reconsider gg = g as Morphism of C by A5;
A41: dom gg = dom g by A2, FUNCT_1:49
.= aa by A40, CAT_1:5 ;
A42: cod (id aa) = aa ;
cod gg = cod g by A3, FUNCT_1:49
.= bb by A40, CAT_1:5 ;
then reconsider gg = gg as Morphism of aa,bb by A41, CAT_1:4;
A43: dom g = a by A40, CAT_1:5;
hence g (*) ii = p . (g,ii) by CAT_1:def_1, A39, A8
.= the Comp of C . (gg,(id aa)) by FUNCT_1:47, A43, A4, A39, A8
.= gg (*) (id aa) by A41, CAT_1:16, A42
.= g by A41, CAT_1:22 ;
::_thesis: verum
end;
thus  ( Hom (b,a) <> {} implies for f being Morphism of b,a holds ii (*) f = f ) ::_thesis: verum
proof
assume A44: Hom (b,a) <> {} ; ::_thesis: for f being Morphism of b,a holds ii (*) f = f
let g be Morphism of b,a; ::_thesis: ii (*) g = g
reconsider gg = g as Morphism of C by A5;
A45: cod gg = cod g by A3, FUNCT_1:49
.= aa by A44, CAT_1:5 ;
A46: dom (id aa) = aa ;
dom gg = dom g by A2, FUNCT_1:49
.= bb by A44, CAT_1:5 ;
then reconsider gg = gg as Morphism of bb,aa by A45, CAT_1:4;
A47: cod g = a by A44, CAT_1:5;
hence ii (*) g = p . (ii,g) by CAT_1:def_1, A38, A8
.= the Comp of C . ((id aa),gg) by FUNCT_1:47, A4, A47, A38, A8
.= (id aa) (*) gg by A45, CAT_1:16, A46
.= g by A45, CAT_1:21 ;
::_thesis: verum
end;
end;
hence  CatStr(# O,M,d,c,p #) is Category by A10, A11, A18, A34; ::_thesis: verum
end;

Lm2:  for C being Category
for O being non empty Subset of the carrier 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 Source of C | M & c = the Target of C | M & p = the Comp of C || M holds
CatStr(# O,M,d,c,p #) is Subcategory of C
proof
let C be Category; ::_thesis: for O being non empty Subset of the carrier 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 Source of C | M & c = the Target of C | M & p = the Comp of C || M holds
CatStr(# O,M,d,c,p #) is Subcategory of C
let O be non empty Subset of the carrier of C; ::_thesis: 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 Source of C | M & c = the Target of C | M & p = the Comp of C || M holds
CatStr(# O,M,d,c,p #) is Subcategory of C
let M be non empty set ; ::_thesis: 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 Source of C | M & c = the Target of C | M & p = the Comp of C || M holds
CatStr(# O,M,d,c,p #) is Subcategory of C
let d, c be Function of M,O; ::_thesis: 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 Source of C | M & c = the Target of C | M & p = the Comp of C || M holds
CatStr(# O,M,d,c,p #) is Subcategory of C
let p be PartFunc of [:M,M:],M; ::_thesis: 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 Source of C | M & c = the Target of C | M & p = the Comp of C || M holds
CatStr(# O,M,d,c,p #) is Subcategory of C
let i be Function of O,M; ::_thesis: ( M = union  {  (Hom (a,b)) where a, b is Object of C : ( a in O & b in O )  }  & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M implies CatStr(# O,M,d,c,p #) is Subcategory of C )
set H =  {  (Hom (a,b)) where a, b is Object of C : ( a in O & b in O )  }  ;
assume that
A1: M = union  {  (Hom (a,b)) where a, b is Object of C : ( a in O & b in O )  }  and
A2: d = the Source of C | M and
A3: c = the Target of C | M and
A4: p = the Comp of C || M ; ::_thesis: CatStr(# O,M,d,c,p #) is Subcategory of C
set B = CatStr(# O,M,d,c,p #);
A5: now__::_thesis:_for_f_being_Morphism_of_CatStr(#_O,M,d,c,p_#)_holds_f_is_Morphism_of_C
let f be Morphism of CatStr(# O,M,d,c,p #); ::_thesis: f is Morphism of C
consider X being set  such that
A6: f in X and
A7: X in  {  (Hom (a,b)) where a, b is Object of C : ( a in O & b in O )  }  by A1, TARSKI:def_4;
 ex a, b being Object of C st
( X = Hom (a,b) & a in O & b in O ) by A7;
hence  f is Morphism of C by A6; ::_thesis: verum
end;
A8: for a, b being Object of CatStr(# O,M,d,c,p #)
for a9, b9 being Object of C st a = a9 & b = b9 holds
Hom (a,b) = Hom (a9,b9)
proof
let a, b be Object of CatStr(# O,M,d,c,p #); ::_thesis: for a9, b9 being Object of C st a = a9 & b = b9 holds
Hom (a,b) = Hom (a9,b9)
let a9, b9 be Object of C; ::_thesis: ( a = a9 & b = b9 implies Hom (a,b) = Hom (a9,b9) )
assume A9: ( a = a9 & b = b9 ) ; ::_thesis: Hom (a,b) = Hom (a9,b9)
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_Hom_(a,b)_implies_x_in_Hom_(a9,b9)_)_&_(_x_in_Hom_(a9,b9)_implies_x_in_Hom_(a,b)_)_)
let x be set ; ::_thesis: ( ( x in Hom (a,b) implies x in Hom (a9,b9) ) & ( x in Hom (a9,b9) implies x in Hom (a,b) ) )
thus  ( x in Hom (a,b) implies x in Hom (a9,b9) ) ::_thesis: ( x in Hom (a9,b9) implies x in Hom (a,b) )
proof
assume A10: x in Hom (a,b) ; ::_thesis: x in Hom (a9,b9)
then reconsider f = x as Morphism of CatStr(# O,M,d,c,p #) ;
reconsider f9 = f as Morphism of C by A5;
 cod f = cod f9 by A3, FUNCT_1:49;
then A11: b = cod f9 by A10, CAT_1:1;
 dom f = dom f9 by A2, FUNCT_1:49;
then  a = dom f9 by A10, CAT_1:1;
hence  x in Hom (a9,b9) by A9, A11; ::_thesis: verum
end;
assume A12: x in Hom (a9,b9) ; ::_thesis: x in Hom (a,b)
then reconsider f9 = x as Morphism of C ;
 Hom (a9,b9) in  {  (Hom (a,b)) where a, b is Object of C : ( a in O & b in O )  }  by A9;
then reconsider f = f9 as Morphism of CatStr(# O,M,d,c,p #) by A1, A12, TARSKI:def_4;
 cod f = cod f9 by A3, FUNCT_1:49;
then A13: cod f = b9 by A12, CAT_1:1;
 dom f = dom f9 by A2, FUNCT_1:49;
then  dom f = a9 by A12, CAT_1:1;
hence  x in Hom (a,b) by A9, A13; ::_thesis: verum
end;
hence  Hom (a,b) = Hom (a9,b9) by TARSKI:1; ::_thesis: verum
end;
reconsider B = CatStr(# O,M,d,c,p #) as Category by Lm1, A1, A2, A3, A4;
A14: for a being Object of B
for a9 being Object of C st a = a9 holds
id a = id a9
proof
let a be Object of B; ::_thesis: for a9 being Object of C st a = a9 holds
id a = id a9
let a9 be Object of C; ::_thesis: ( a = a9 implies id a = id a9 )
assume A15: a = a9 ; ::_thesis: id a = id a9
A16: Hom (a9,a9) in  {  (Hom (a,b)) where a, b is Object of C : ( a in O & b in O )  }  by A15;
A17: id a9 in Hom (a9,a9) by CAT_1:27;
then reconsider ii = id a9 as Morphism of B by A16, A1, TARSKI:def_4;
A18: dom ii = dom (id a9) by A2, FUNCT_1:49
.= a9 ;
A19: cod ii = cod (id a9) by A3, FUNCT_1:49
.= a9 ;
 ii in Hom (a,a) by A17, A8, A15;
then reconsider ii = ii as Morphism of a,a by CAT_1:def_5;
A20: for f, g being Morphism of B holds
( [g,f] in dom p iff d . g = c . f )
proof
let f, g be Morphism of B; ::_thesis: ( [g,f] in dom p iff d . g = c . f )
reconsider gg = g, ff = f as Morphism of C by A5;
A21: ( d . g = dom gg & c . f = cod ff ) by A2, A3, FUNCT_1:49;
thus  ( [g,f] in dom p implies d . g = c . f ) ::_thesis: ( d . g = c . f implies [g,f] in dom p )
proof
assume  [g,f] in dom p ; ::_thesis: d . g = c . f
then  [g,f] in (dom the Comp of C) /\ [:M,M:] by A4, RELAT_1:61;
then  [gg,ff] in dom the Comp of C by XBOOLE_0:def_4;
hence  d . g = c . f by A21, CAT_1:def_6; ::_thesis: verum
end;
assume  d . g = c . f ; ::_thesis: [g,f] in dom p
then  [g,f] in dom the Comp of C by A21, CAT_1:def_6;
then  [g,f] in (dom the Comp of C) /\ [:M,M:] by XBOOLE_0:def_4;
hence  [g,f] in dom p by A4, RELAT_1:61; ::_thesis: verum
end;
 for b being Object of B holds
( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) ii = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds ii (*) f = f ) )
proof
let b be Object of B; ::_thesis: ( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) ii = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds ii (*) f = f ) )
 b in O ;
then reconsider bb = b as Element of C ;
thus  ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) ii = f ) ::_thesis: ( Hom (b,a) <> {} implies for f being Morphism of b,a holds ii (*) f = f )
proof
assume A22: Hom (a,b) <> {} ; ::_thesis: for f being Morphism of a,b holds f (*) ii = f
let g be Morphism of a,b; ::_thesis: g (*) ii = g
reconsider gg = g as Morphism of C by A5;
A23: dom gg = dom g by A2, FUNCT_1:49
.= a9 by A15, CAT_1:5, A22 ;
A24: cod (id a9) = a9 ;
cod gg = cod g by A3, FUNCT_1:49
.= bb by A22, CAT_1:5 ;
then reconsider gg = gg as Morphism of a9,bb by A23, CAT_1:4;
A25: dom g = a by A22, CAT_1:5;
hence g (*) ii = p . (g,ii) by CAT_1:def_1, A19, A20, A15
.= the Comp of C . (gg,(id a9)) by FUNCT_1:47, A19, A20, A15, A4, A25
.= gg (*) (id a9) by A23, CAT_1:16, A24
.= g by A23, CAT_1:22 ;
::_thesis: verum
end;
assume A26: Hom (b,a) <> {} ; ::_thesis: for f being Morphism of b,a holds ii (*) f = f
let g be Morphism of b,a; ::_thesis: ii (*) g = g
reconsider gg = g as Morphism of C by A5;
A27: cod gg = cod g by A3, FUNCT_1:49
.= a9 by A15, CAT_1:5, A26 ;
A28: dom (id a9) = a9 ;
dom gg = dom g by A2, FUNCT_1:49
.= bb by A26, CAT_1:5 ;
then reconsider gg = gg as Morphism of bb,a9 by A27, CAT_1:4;
A29: cod g = a by A26, CAT_1:5;
hence ii (*) g = p . (ii,g) by CAT_1:def_1, A18, A20, A15
.= the Comp of C . ((id a9),gg) by FUNCT_1:47, A18, A20, A15, A4, A29
.= (id a9) (*) gg by A27, CAT_1:16, A28
.= g by A27, CAT_1:21 ;
::_thesis: verum
end;
hence  id a = id a9 by CAT_1:def_12; ::_thesis: verum
end;
 ( ( for a, b being Object of B
for a9, b9 being Object of C st a = a9 & b = b9 holds
Hom (a,b) c= Hom (a9,b9) ) & the Comp of B c= the Comp of C ) by A4, A8, RELAT_1:59;
hence  CatStr(# O,M,d,c,p #) is Subcategory of C by A14, Def4; ::_thesis: verum
end;

theorem :: CAT_2:21
for C being Category
for O being non empty Subset of the carrier 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 Source of C | M & c = the Target of C | M & p = the Comp of C || M holds
CatStr(# O,M,d,c,p #) is full Subcategory of C
proof
let C be Category; ::_thesis: for O being non empty Subset of the carrier 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 Source of C | M & c = the Target of C | M & p = the Comp of C || M holds
CatStr(# O,M,d,c,p #) is full Subcategory of C
let O be non empty Subset of the carrier of C; ::_thesis: 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 Source of C | M & c = the Target of C | M & p = the Comp of C || M holds
CatStr(# O,M,d,c,p #) is full Subcategory of C
let M be non empty set ; ::_thesis: 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 Source of C | M & c = the Target of C | M & p = the Comp of C || M holds
CatStr(# O,M,d,c,p #) is full Subcategory of C
let d, c be Function of M,O; ::_thesis: 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 Source of C | M & c = the Target of C | M & p = the Comp of C || M holds
CatStr(# O,M,d,c,p #) is full Subcategory of C
let p be PartFunc of [:M,M:],M; ::_thesis: 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 Source of C | M & c = the Target of C | M & p = the Comp of C || M holds
CatStr(# O,M,d,c,p #) is full Subcategory of C
let i be Function of O,M; ::_thesis: ( M = union  {  (Hom (a,b)) where a, b is Object of C : ( a in O & b in O )  }  & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M implies CatStr(# O,M,d,c,p #) is full Subcategory of C )
set H =  {  (Hom (a,b)) where a, b is Object of C : ( a in O & b in O )  }  ;
assume that
A1: M = union  {  (Hom (a,b)) where a, b is Object of C : ( a in O & b in O )  }  and
A2: d = the Source of C | M and
A3: c = the Target of C | M and
A4: p = the Comp of C || M ; ::_thesis: CatStr(# O,M,d,c,p #) is full Subcategory of C
set B = CatStr(# O,M,d,c,p #);
A5: now__::_thesis:_for_f_being_Morphism_of_CatStr(#_O,M,d,c,p_#)_holds_f_is_Morphism_of_C
let f be Morphism of CatStr(# O,M,d,c,p #); ::_thesis: f is Morphism of C
consider X being set  such that
A6: f in X and
A7: X in  {  (Hom (a,b)) where a, b is Object of C : ( a in O & b in O )  }  by A1, TARSKI:def_4;
 ex a, b being Object of C st
( X = Hom (a,b) & a in O & b in O ) by A7;
hence  f is Morphism of C by A6; ::_thesis: verum
end;
A8: for a, b being Object of CatStr(# O,M,d,c,p #)
for a9, b9 being Object of C st a = a9 & b = b9 holds
Hom (a,b) = Hom (a9,b9)
proof
let a, b be Object of CatStr(# O,M,d,c,p #); ::_thesis: for a9, b9 being Object of C st a = a9 & b = b9 holds
Hom (a,b) = Hom (a9,b9)
let a9, b9 be Object of C; ::_thesis: ( a = a9 & b = b9 implies Hom (a,b) = Hom (a9,b9) )
assume A9: ( a = a9 & b = b9 ) ; ::_thesis: Hom (a,b) = Hom (a9,b9)
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_Hom_(a,b)_implies_x_in_Hom_(a9,b9)_)_&_(_x_in_Hom_(a9,b9)_implies_x_in_Hom_(a,b)_)_)
let x be set ; ::_thesis: ( ( x in Hom (a,b) implies x in Hom (a9,b9) ) & ( x in Hom (a9,b9) implies x in Hom (a,b) ) )
thus  ( x in Hom (a,b) implies x in Hom (a9,b9) ) ::_thesis: ( x in Hom (a9,b9) implies x in Hom (a,b) )
proof
assume A10: x in Hom (a,b) ; ::_thesis: x in Hom (a9,b9)
then reconsider f = x as Morphism of CatStr(# O,M,d,c,p #) ;
reconsider f9 = f as Morphism of C by A5;
 cod f = cod f9 by A3, FUNCT_1:49;
then A11: b = cod f9 by A10, CAT_1:1;
 dom f = dom f9 by A2, FUNCT_1:49;
then  a = dom f9 by A10, CAT_1:1;
hence  x in Hom (a9,b9) by A9, A11; ::_thesis: verum
end;
assume A12: x in Hom (a9,b9) ; ::_thesis: x in Hom (a,b)
then reconsider f9 = x as Morphism of C ;
 Hom (a9,b9) in  {  (Hom (a,b)) where a, b is Object of C : ( a in O & b in O )  }  by A9;
then reconsider f = f9 as Morphism of CatStr(# O,M,d,c,p #) by A1, A12, TARSKI:def_4;
 cod f = cod f9 by A3, FUNCT_1:49;
then A13: cod f = b9 by A12, CAT_1:1;
 dom f = dom f9 by A2, FUNCT_1:49;
then  dom f = a9 by A12, CAT_1:1;
hence  x in Hom (a,b) by A9, A13; ::_thesis: verum
end;
hence  Hom (a,b) = Hom (a9,b9) by TARSKI:1; ::_thesis: verum
end;
reconsider B = CatStr(# O,M,d,c,p #) as Subcategory of C by Lm2, A1, A2, A3, A4;
 B is full by A8, Def6;
hence  CatStr(# O,M,d,c,p #) is full Subcategory of C ; ::_thesis: verum
end;

theorem :: CAT_2:22
for C being Category
for O being non empty Subset of the carrier of C
for M being non empty set
for d, c being Function of M,O
for p being PartFunc of [:M,M:],M st CatStr(# O,M,d,c,p #) 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 Source of C | M & c = the Target of C | M & p = the Comp of C || M )
proof
let C be Category; ::_thesis: for O being non empty Subset of the carrier of C
for M being non empty set
for d, c being Function of M,O
for p being PartFunc of [:M,M:],M st CatStr(# O,M,d,c,p #) 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 Source of C | M & c = the Target of C | M & p = the Comp of C || M )
let O be non empty Subset of the carrier of C; ::_thesis: for M being non empty set
for d, c being Function of M,O
for p being PartFunc of [:M,M:],M st CatStr(# O,M,d,c,p #) 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 Source of C | M & c = the Target of C | M & p = the Comp of C || M )
let M be non empty set ; ::_thesis: for d, c being Function of M,O
for p being PartFunc of [:M,M:],M st CatStr(# O,M,d,c,p #) 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 Source of C | M & c = the Target of C | M & p = the Comp of C || M )
let d, c be Function of M,O; ::_thesis: for p being PartFunc of [:M,M:],M st CatStr(# O,M,d,c,p #) 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 Source of C | M & c = the Target of C | M & p = the Comp of C || M )
let p be PartFunc of [:M,M:],M; ::_thesis: ( CatStr(# O,M,d,c,p #) is full Subcategory of C implies ( M = union  {  (Hom (a,b)) where a, b is Object of C : ( a in O & b in O )  }  & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M ) )
set H =  {  (Hom (a,b)) where a, b is Object of C : ( a in O & b in O )  }  ;
set B = CatStr(# O,M,d,c,p #);
assume A1: CatStr(# O,M,d,c,p #) is full Subcategory of C ; ::_thesis: ( M = union  {  (Hom (a,b)) where a, b is Object of C : ( a in O & b in O )  }  & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M )
A2: for f being Morphism of CatStr(# O,M,d,c,p #) holds
( d . f = the Source of C . f & c . f = the Target of C . f )
proof
let f be Morphism of CatStr(# O,M,d,c,p #); ::_thesis: ( d . f = the Source of C . f & c . f = the Target of C . f )
reconsider f9 = f as Morphism of C by A1, Th8;
 ( dom f = dom f9 & cod f = cod f9 ) by A1, Th9;
hence  ( d . f = the Source of C . f & c . f = the Target of C . f ) ; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_M_implies_x_in_union__{__(Hom_(a,b))_where_a,_b_is_Object_of_C_:_(_a_in_O_&_b_in_O_)__}__)_&_(_x_in_union__{__(Hom_(a,b))_where_a,_b_is_Object_of_C_:_(_a_in_O_&_b_in_O_)__}__implies_x_in_M_)_)
let x be set ; ::_thesis: ( ( x in M implies x in union  {  (Hom (a,b)) where a, b is Object of C : ( a in O & b in O )  }  ) & ( x in union  {  (Hom (a,b)) where a, b is Object of C : ( a in O & b in O )  }  implies x in M ) )
thus  ( x in M implies x in union  {  (Hom (a,b)) where a, b is Object of C : ( a in O & b in O )  }  ) ::_thesis: ( x in union  {  (Hom (a,b)) where a, b is Object of C : ( a in O & b in O )  }  implies x in M )
proof
assume  x in M ; ::_thesis: x in union  {  (Hom (a,b)) where a, b is Object of C : ( a in O & b in O )  }
then reconsider f = x as Morphism of CatStr(# O,M,d,c,p #) ;
reconsider f9 = f as Morphism of C by A1, Th8;
set a9 = dom f9;
set b9 = cod f9;
 ( the Source of CatStr(# O,M,d,c,p #) . f = the Source of C . f9 & the Target of CatStr(# O,M,d,c,p #) . f = the Target of C . f9 ) by A2;
then  ( f in Hom ((dom f9),(cod f9)) & Hom ((dom f9),(cod f9)) in  {  (Hom (a,b)) where a, b is Object of C : ( a in O & b in O )  }  ) ;
hence  x in union  {  (Hom (a,b)) where a, b is Object of C : ( a in O & b in O )  }  by TARSKI:def_4; ::_thesis: verum
end;
assume  x in union  {  (Hom (a,b)) where a, b is Object of C : ( a in O & b in O )  }  ; ::_thesis: x in M
then consider X being set  such that
A3: x in X and
A4: X in  {  (Hom (a,b)) where a, b is Object of C : ( a in O & b in O )  }  by TARSKI:def_4;
consider a9, b9 being Object of C such that
A5: X = Hom (a9,b9) and
A6: ( a9 in O & b9 in O ) by A4;
reconsider a = a9, b = b9 as Object of CatStr(# O,M,d,c,p #) by A6;
 Hom (a,b) = Hom (a9,b9) by A1, Def6;
hence  x in M by A3, A5; ::_thesis: verum
end;
hence  M = union  {  (Hom (a,b)) where a, b is Object of C : ( a in O & b in O )  }  by TARSKI:1; ::_thesis: ( d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M )
then reconsider d9 = the Source of C | M, c9 = the Target of C | M as Function of M,O by Th20;
set p9 = the Comp of C || M;
now__::_thesis:_for_f_being_Element_of_M_holds_d_._f_=_d9_._f
let f be Element of M; ::_thesis: d . f = d9 . f
 d . f = the Source of C . f by A2;
hence  d . f = d9 . f by FUNCT_1:49; ::_thesis: verum
end;
hence  d = the Source of C | M by FUNCT_2:63; ::_thesis: ( c = the Target of C | M & p = the Comp of C || M )
now__::_thesis:_for_f_being_Element_of_M_holds_c_._f_=_c9_._f
let f be Element of M; ::_thesis: c . f = c9 . f
 c . f = the Target of C . f by A2;
hence  c . f = c9 . f by FUNCT_1:49; ::_thesis: verum
end;
hence  c = the Target of C | M by FUNCT_2:63; ::_thesis: p = the Comp of C || M
now__::_thesis:_(_dom_p_=_dom_(_the_Comp_of_C_||_M)_&_(_for_x_being_set_st_x_in_dom_p_holds_
p_._x_=_(_the_Comp_of_C_||_M)_._x_)_)
A7: dom p c= [:M,M:] by RELAT_1:def_18;
A8: dom ( the Comp of C || M) = (dom the Comp of C) /\ [:M,M:] by RELAT_1:61;
 the Comp of CatStr(# O,M,d,c,p #) c= the Comp of C by A1, Def4;
then  dom p c= dom the Comp of C by GRFUNC_1:2;
then A9: dom p c= dom ( the Comp of C || M) by A7, A8, XBOOLE_1:19;
 dom ( the Comp of C || M) c= dom p
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom ( the Comp of C || M) or x in dom p )
assume A10: x in dom ( the Comp of C || M) ; ::_thesis: x in dom p
then  x in [:M,M:] by A8, XBOOLE_0:def_4;
then consider g, f being Element of M such that
A11: x = [g,f] by DOMAIN_1:1;
reconsider f = f, g = g as Morphism of CatStr(# O,M,d,c,p #) ;
reconsider f9 = f, g9 = g as Morphism of C by A1, Th8;
 [g,f] in dom the Comp of C by A8, A10, A11, XBOOLE_0:def_4;
then A12: dom g9 = cod f9 by CAT_1:15;
 ( cod f = cod f9 & dom g = dom g9 ) by A1, Th9;
hence  x in dom p by A1, A11, A12, CAT_1:15; ::_thesis: verum
end;
hence  dom p = dom ( the Comp of C || M) by A9, XBOOLE_0:def_10; ::_thesis: for x being set st x in dom p holds
p . x = ( the Comp of C || M) . x
let x be set ; ::_thesis: ( x in dom p implies p . x = ( the Comp of C || M) . x )
assume A13: x in dom p ; ::_thesis: p . x = ( the Comp of C || M) . x
then consider g, f being Element of M such that
A14: x = [g,f] by A7, DOMAIN_1:1;
reconsider f = f, g = g as Morphism of CatStr(# O,M,d,c,p #) ;
A15: dom g = cod f by A1, A13, A14, CAT_1:15;
reconsider f9 = f, g9 = g as Morphism of C by A1, Th8;
A16: ( cod f = cod f9 & dom g = dom g9 ) by A1, Th9;
 p . x = p . (g,f) by A14;
hence p . x = g (*) f by A1, A15, CAT_1:16
.= g9 (*) f9 by A1, A15, Th11
.= the Comp of C . (g9,f9) by A16, A1, A13, A14, CAT_1:15, CAT_1:16
.= ( the Comp of C || M) . x by A9, A13, A14, FUNCT_1:47 ;
::_thesis: verum
end;
hence  p = the Comp of C || M by FUNCT_1:2; ::_thesis: verum
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
 [:f1,f2:] is Function of [:X1,X2:],[:Y1,Y2:] ;
hence  [:f1,f2:] is Function of [:X1,X2:],[:Y1,Y2:] ; ::_thesis: verum
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:59;
end;

definition
let C, D be Category;
func[:C,D:] ->  Category equals :: CAT_2:def 7
 CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #);
coherence
 CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) is Category
proof
set O = [: the carrier of C, the carrier of D:];
set M = [: the carrier' of C, the carrier' of D:];
set d = [: the Source of C, the Source of D:];
set c = [: the Target of C, the Target of D:];
set p = |: the Comp of C, the Comp of D:|;
A1: for f, g being Element of [: the carrier' of C, the carrier' of D:] st [: the Source of C, the Source of D:] . g = [: the Target of C, the Target of D:] . f holds
( [(g `1),(f `1)] in dom the Comp of C & [(g `2),(f `2)] in dom the Comp of D )
proof
let f, g be Element of [: the carrier' of C, the carrier' of D:]; ::_thesis: ( [: the Source of C, the Source of D:] . g = [: the Target of C, the Target of D:] . f implies ( [(g `1),(f `1)] in dom the Comp of C & [(g `2),(f `2)] in dom the Comp of D ) )
A2: ( [: the Source of C, the Source of D:] . ((g `1),(g `2)) = [( the Source of C . (g `1)),( the Source of D . (g `2))] & [: the Target of C, the Target of D:] . ((f `1),(f `2)) = [( the Target of C . (f `1)),( the Target of D . (f `2))] ) by FUNCT_3:75;
assume A3: [: the Source of C, the Source of D:] . g = [: the Target of C, the Target of D:] . f ; ::_thesis: ( [(g `1),(f `1)] in dom the Comp of C & [(g `2),(f `2)] in dom the Comp of D )
 ( g = [(g `1),(g `2)] & f = [(f `1),(f `2)] ) by MCART_1:21;
then  ( dom (g `1) = cod (f `1) & dom (g `2) = cod (f `2) ) by A2, A3, XTUPLE_0:1;
hence  ( [(g `1),(f `1)] in dom the Comp of C & [(g `2),(f `2)] in dom the Comp of D ) by CAT_1:def_6; ::_thesis: verum
end;
A4: for f, g being Element of [: the carrier' of C, the carrier' of D:] st [g,f] in dom |: the Comp of C, the Comp of D:| holds
( dom (g `1) = cod (f `1) & dom (g `2) = cod (f `2) )
proof
let f, g be Element of [: the carrier' of C, the carrier' of D:]; ::_thesis: ( [g,f] in dom |: the Comp of C, the Comp of D:| implies ( dom (g `1) = cod (f `1) & dom (g `2) = cod (f `2) ) )
assume A5: [g,f] in dom |: the Comp of C, the Comp of D:| ; ::_thesis: ( dom (g `1) = cod (f `1) & dom (g `2) = cod (f `2) )
 ( g = [(g `1),(g `2)] & f = [(f `1),(f `2)] ) by MCART_1:21;
then  ( [(g `1),(f `1)] in dom the Comp of C & [(g `2),(f `2)] in dom the Comp of D ) by A5, FUNCT_4:54;
hence  ( dom (g `1) = cod (f `1) & dom (g `2) = cod (f `2) ) by CAT_1:def_6; ::_thesis: verum
end;
set B = CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #);
A6: CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) is Category-like
proof
let ff, gg be Morphism of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #); :: according to CAT_1:def_6 ::_thesis: ( ( not [gg,ff] in dom the Comp of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) or dom gg = cod ff ) & ( not dom gg = cod ff or [gg,ff] in dom the Comp of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) ) )
reconsider f = ff, g = gg as Element of [: the carrier' of C, the carrier' of D:] ;
A7: ( g = [(g `1),(g `2)] & f = [(f `1),(f `2)] ) by MCART_1:21;
thus  ( [gg,ff] in dom the Comp of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) implies dom gg = cod ff ) ::_thesis: ( not dom gg = cod ff or [gg,ff] in dom the Comp of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) )
proof
A8: ( [: the Source of C, the Source of D:] . ((g `1),(g `2)) = [(dom (g `1)),(dom (g `2))] & [: the Target of C, the Target of D:] . ((f `1),(f `2)) = [(cod (f `1)),(cod (f `2))] ) by FUNCT_3:75;
assume A9: [gg,ff] in dom the Comp of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) ; ::_thesis: dom gg = cod ff
then  dom (g `1) = cod (f `1) by A4;
hence  dom gg = cod ff by A4, A7, A9, A8; ::_thesis: verum
end;
assume  dom gg = cod ff ; ::_thesis: [gg,ff] in dom the Comp of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #)
then  ( [(g `1),(f `1)] in dom the Comp of C & [(g `2),(f `2)] in dom the Comp of D ) by A1;
hence  [gg,ff] in dom the Comp of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) by A7, FUNCT_4:54; ::_thesis: verum
end;
A10: for f, g being Morphism of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) holds
( [g,f] in dom the Comp of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) iff dom g = cod f ) by A6, CAT_1:def_6;
A11: for f, g being Element of [: the carrier' of C, the carrier' of D:] st [: the Source of C, the Source of D:] . g = [: the Target of C, the Target of D:] . f holds
|: the Comp of C, the Comp of D:| . (g,f) = [( the Comp of C . ((g `1),(f `1))),( the Comp of D . ((g `2),(f `2)))]
proof
let f, g be Element of [: the carrier' of C, the carrier' of D:]; ::_thesis: ( [: the Source of C, the Source of D:] . g = [: the Target of C, the Target of D:] . f implies |: the Comp of C, the Comp of D:| . (g,f) = [( the Comp of C . ((g `1),(f `1))),( the Comp of D . ((g `2),(f `2)))] )
reconsider ff = f, gg = g as Morphism of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) ;
assume  [: the Source of C, the Source of D:] . g = [: the Target of C, the Target of D:] . f ; ::_thesis: |: the Comp of C, the Comp of D:| . (g,f) = [( the Comp of C . ((g `1),(f `1))),( the Comp of D . ((g `2),(f `2)))]
then A12: dom gg = cod ff ;
 ( g = [(g `1),(g `2)] & f = [(f `1),(f `2)] ) by MCART_1:21;
hence  |: the Comp of C, the Comp of D:| . (g,f) = [( the Comp of C . ((g `1),(f `1))),( the Comp of D . ((g `2),(f `2)))] by A12, A10, FUNCT_4:55; ::_thesis: verum
end;
A13: for f, g being Element of [: the carrier' of C, the carrier' of D:] st [: the Source of C, the Source of D:] . g = [: the Target of C, the Target of D:] . f holds
( [: the Source of C, the Source of D:] . (|: the Comp of C, the Comp of D:| . (g,f)) = [: the Source of C, the Source of D:] . f & [: the Target of C, the Target of D:] . (|: the Comp of C, the Comp of D:| . (g,f)) = [: the Target of C, the Target of D:] . g )
proof
let f, g be Element of [: the carrier' of C, the carrier' of D:]; ::_thesis: ( [: the Source of C, the Source of D:] . g = [: the Target of C, the Target of D:] . f implies ( [: the Source of C, the Source of D:] . (|: the Comp of C, the Comp of D:| . (g,f)) = [: the Source of C, the Source of D:] . f & [: the Target of C, the Target of D:] . (|: the Comp of C, the Comp of D:| . (g,f)) = [: the Target of C, the Target of D:] . g ) )
reconsider ff = f, gg = g as Morphism of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) ;
A14: ( f = [(f `1),(f `2)] & [: the Source of C, the Source of D:] . ((f `1),(f `2)) = [(dom (f `1)),(dom (f `2))] ) by FUNCT_3:75, MCART_1:21;
assume A15: [: the Source of C, the Source of D:] . g = [: the Target of C, the Target of D:] . f ; ::_thesis: ( [: the Source of C, the Source of D:] . (|: the Comp of C, the Comp of D:| . (g,f)) = [: the Source of C, the Source of D:] . f & [: the Target of C, the Target of D:] . (|: the Comp of C, the Comp of D:| . (g,f)) = [: the Target of C, the Target of D:] . g )
then A16: the Comp of C . [(g `1),(f `1)] in the carrier' of C by A1, PARTFUN1:4;
then A17: the Comp of C . ((g `1),(f `1)) in dom the Source of C by FUNCT_2:def_1;
 dom gg = cod ff by A15;
then A18: [gg,ff] in dom |: the Comp of C, the Comp of D:| by A6, CAT_1:def_6;
then A19: dom (g `1) = cod (f `1) by A4;
then  [(g `1),(f `1)] in dom the Comp of C by CAT_1:def_6;
then A20: the Comp of C . ((g `1),(f `1)) = (g `1) (*) (f `1) by CAT_1:def_1;
A21: dom ((g `1) (*) (f `1)) = dom (f `1) by A19, CAT_1:def_7;
A22: the Comp of D . [(g `2),(f `2)] in the carrier' of D by A1, A15, PARTFUN1:4;
then A23: the Comp of D . ((g `2),(f `2)) in dom the Source of D by FUNCT_2:def_1;
A24: dom (g `2) = cod (f `2) by A4, A18;
then  [(g `2),(f `2)] in dom the Comp of D by CAT_1:def_6;
then A25: the Comp of D . ((g `2),(f `2)) = (g `2) (*) (f `2) by CAT_1:def_1;
A26: dom ((g `2) (*) (f `2)) = dom (f `2) by A24, CAT_1:def_7;
thus [: the Source of C, the Source of D:] . (|: the Comp of C, the Comp of D:| . (g,f)) = [: the Source of C, the Source of D:] . (( the Comp of C . ((g `1),(f `1))),( the Comp of D . ((g `2),(f `2)))) by A11, A15
.= [: the Source of C, the Source of D:] . f by A14, A21, A26, A17, A23, A20, A25, FUNCT_3:def_8 ; ::_thesis: [: the Target of C, the Target of D:] . (|: the Comp of C, the Comp of D:| . (g,f)) = [: the Target of C, the Target of D:] . g
A27: ( g = [(g `1),(g `2)] & [: the Target of C, the Target of D:] . ((g `1),(g `2)) = [( the Target of C . (g `1)),( the Target of D . (g `2))] ) by FUNCT_3:75, MCART_1:21;
A28: cod ((g `2) (*) (f `2)) = cod (g `2) by A24, CAT_1:def_7;
A29: cod ((g `1) (*) (f `1)) = cod (g `1) by A19, CAT_1:def_7;
A30: the Comp of D . ((g `2),(f `2)) in dom the Target of D by A22, FUNCT_2:def_1;
A31: the Comp of C . ((g `1),(f `1)) in dom the Target of C by A16, FUNCT_2:def_1;
thus [: the Target of C, the Target of D:] . (|: the Comp of C, the Comp of D:| . (g,f)) = [: the Target of C, the Target of D:] . (( the Comp of C . ((g `1),(f `1))),( the Comp of D . ((g `2),(f `2)))) by A11, A15
.= [: the Target of C, the Target of D:] . g by A27, A29, A28, A31, A30, A20, A25, FUNCT_3:def_8 ; ::_thesis: verum
end;
A32: CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) is transitive
proof
let ff, gg be Morphism of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #); :: according to CAT_1:def_7 ::_thesis: ( not dom gg = cod ff or ( dom (gg (*) ff) = dom ff & cod (gg (*) ff) = cod gg ) )
reconsider f = ff, g = gg as Element of [: the carrier' of C, the carrier' of D:] ;
assume A33: dom gg = cod ff ; ::_thesis: ( dom (gg (*) ff) = dom ff & cod (gg (*) ff) = cod gg )
then A34: the Comp of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) . (gg,ff) = gg (*) ff by A10, CAT_1:def_1;
thus  dom (gg (*) ff) = dom ff by A13, A33, A34; ::_thesis: cod (gg (*) ff) = cod gg
thus  cod (gg (*) ff) = cod gg by A13, A33, A34; ::_thesis: verum
end;
A35: CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) is associative
proof
let ff, gg, hh be Morphism of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #); :: according to CAT_1:def_8 ::_thesis: ( not dom hh = cod gg or not dom gg = cod ff or hh (*) (gg (*) ff) = (hh (*) gg) (*) ff )
reconsider f = ff, g = gg, h = hh as Element of [: the carrier' of C, the carrier' of D:] ;
assume that
A36: dom hh = cod gg and
A37: dom gg = cod ff ; ::_thesis: hh (*) (gg (*) ff) = (hh (*) gg) (*) ff
A38: ( the Comp of C . [(h `1),(g `1)] in the carrier' of C & the Comp of D . [(h `2),(g `2)] in the carrier' of D ) by A1, A36, PARTFUN1:4;
 ( the Comp of C . [(g `1),(f `1)] in the carrier' of C & the Comp of D . [(g `2),(f `2)] in the carrier' of D ) by A1, A37, PARTFUN1:4;
then reconsider pgf = [( the Comp of C . [(g `1),(f `1)]),( the Comp of D . [(g `2),(f `2)])], phg = [( the Comp of C . [(h `1),(g `1)]),( the Comp of D . [(h `2),(g `2)])] as Element of [: the carrier' of C, the carrier' of D:] by A38, ZFMISC_1:87;
set pgf2 = pgf `2 ;
set phg2 = phg `2 ;
set pgf1 = pgf `1 ;
set phg1 = phg `1 ;
A39: |: the Comp of C, the Comp of D:| . (g,f) = [( the Comp of C . ((g `1),(f `1))),( the Comp of D . ((g `2),(f `2)))] by A11, A37;
A40: [: the Source of C, the Source of D:] . h = [: the Target of C, the Target of D:] . (|: the Comp of C, the Comp of D:| . (g,f)) by A13, A36, A37;
A41: |: the Comp of C, the Comp of D:| . (h,g) = [( the Comp of C . ((h `1),(g `1))),( the Comp of D . ((h `2),(g `2)))] by A11, A36;
 [(h `2),(g `2)] in dom the Comp of D by A1, A36;
then A42: dom (h `2) = cod (g `2) by CAT_1:def_6;
 [(h `1),(g `1)] in dom the Comp of C by A1, A36;
then A43: dom (h `1) = cod (g `1) by CAT_1:def_6;
 [(g `2),(f `2)] in dom the Comp of D by A1, A37;
then A44: dom (g `2) = cod (f `2) by CAT_1:def_6;
 [(g `1),(f `1)] in dom the Comp of C by A1, A37;
then A45: dom (g `1) = cod (f `1) by CAT_1:def_6;
A46: [: the Source of C, the Source of D:] . (|: the Comp of C, the Comp of D:| . (h,g)) = [: the Target of C, the Target of D:] . f by A13, A36, A37;
A47: ( pgf `1 = the Comp of C . ((g `1),(f `1)) & phg `1 = the Comp of C . ((h `1),(g `1)) ) by MCART_1:7;
A48: ( pgf `2 = the Comp of D . ((g `2),(f `2)) & phg `2 = the Comp of D . ((h `2),(g `2)) ) by MCART_1:7;
A49: (h `2) (*) ((g `2) (*) (f `2)) = ((h `2) (*) (g `2)) (*) (f `2) by A42, A44, CAT_1:def_8;
A50: gg (*) ff = |: the Comp of C, the Comp of D:| . (g,f) by A37, A10, CAT_1:def_1;
then A51: cod (gg (*) ff) = dom hh by A13, A36, A37;
A52: hh (*) gg = |: the Comp of C, the Comp of D:| . (h,g) by A36, A10, CAT_1:def_1;
then A53: dom (hh (*) gg) = cod ff by A13, A36, A37;
A54: cod ((g `1) (*) (f `1)) = cod (g `1) by A45, CAT_1:def_7;
A55: pgf `1 = (g `1) (*) (f `1) by A47, A45, CAT_1:16;
A56: cod ((g `2) (*) (f `2)) = cod (g `2) by A44, CAT_1:def_7;
 pgf `2 = (g `2) (*) (f `2) by A48, A44, CAT_1:16;
then A57: the Comp of D . ((h `2),(pgf `2)) = (h `2) (*) ((g `2) (*) (f `2)) by A42, A56, CAT_1:16;
A58: dom ((h `1) (*) (g `1)) = dom (g `1) by A43, CAT_1:def_7;
A59: phg `1 = (h `1) (*) (g `1) by A47, A43, CAT_1:16;
A60: dom ((h `2) (*) (g `2)) = dom (g `2) by A42, CAT_1:def_7;
 phg `2 = (h `2) (*) (g `2) by A48, A42, CAT_1:16;
then A61: the Comp of D . ((phg `2),(f `2)) = ((h `2) (*) (g `2)) (*) (f `2) by A44, A60, CAT_1:16;
thus hh (*) (gg (*) ff) = |: the Comp of C, the Comp of D:| . (h,(|: the Comp of C, the Comp of D:| . (g,f))) by A51, A50, A10, CAT_1:def_1
.= [( the Comp of C . ((h `1),(pgf `1))),( the Comp of D . ((h `2),(pgf `2)))] by A40, A11, A39
.= [((h `1) (*) ((g `1) (*) (f `1))),((h `2) (*) ((g `2) (*) (f `2)))] by A55, A57, A43, A54, CAT_1:16
.= [(((h `1) (*) (g `1)) (*) (f `1)),(((h `2) (*) (g `2)) (*) (f `2))] by A43, A45, A49, CAT_1:def_8
.= [( the Comp of C . ((phg `1),(f `1))),( the Comp of D . ((phg `2),(f `2)))] by A59, A61, A45, A58, CAT_1:16
.= |: the Comp of C, the Comp of D:| . ((|: the Comp of C, the Comp of D:| . (h,g)),f) by A46, A11, A41
.= (hh (*) gg) (*) ff by A53, A10, A52, CAT_1:def_1 ; ::_thesis: verum
end;
A62: CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) is reflexive
proof
let b be Element of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #); :: according to CAT_1:def_9 ::_thesis: not Hom (b,b) = {}
reconsider bb = b as Element of [: the carrier of C, the carrier of D:] ;
reconsider ii = [(id (bb `1)),(id (bb `2))] as Morphism of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) ;
A63: cod ii = [: the Target of C, the Target of D:] . ((id (bb `1)),(id (bb `2)))
.= [(cod (id (bb `1))),(cod (id (bb `2)))] by FUNCT_3:75
.= [(bb `1),(cod (id (bb `2)))]
.= [(bb `1),(bb `2)]
.= bb by MCART_1:21 ;
dom ii = [: the Source of C, the Source of D:] . ((id (bb `1)),(id (bb `2)))
.= [(dom (id (bb `1))),(dom (id (bb `2)))] by FUNCT_3:75
.= [(bb `1),(dom (id (bb `2)))]
.= [(bb `1),(bb `2)]
.= bb by MCART_1:21 ;
then  [(id (bb `1)),(id (bb `2))] in Hom (b,b) by A63;
hence  Hom (b,b) <> {} ; ::_thesis: verum
end;
 CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) is with_identities
proof
let a be Element of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #); :: according to CAT_1:def_10 ::_thesis: ex b1 being Morphism of a,a st
for b2 being Element of the carrier of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) holds
( ( Hom (a,b2) = {} or for b3 being Morphism of a,b2 holds b3 (*) b1 = b3 ) & ( Hom (b2,a) = {} or for b3 being Morphism of b2,a holds b1 (*) b3 = b3 ) )
reconsider aa = a as Element of [: the carrier of C, the carrier of D:] ;
reconsider ii = [(id (aa `1)),(id (aa `2))] as Morphism of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) ;
A64: cod ii = [: the Target of C, the Target of D:] . ((id (aa `1)),(id (aa `2)))
.= [(cod (id (aa `1))),(cod (id (aa `2)))] by FUNCT_3:75
.= [(aa `1),(cod (id (aa `2)))]
.= [(aa `1),(aa `2)]
.= aa by MCART_1:21 ;
A65: dom ii = [: the Source of C, the Source of D:] . ((id (aa `1)),(id (aa `2)))
.= [(dom (id (aa `1))),(dom (id (aa `2)))] by FUNCT_3:75
.= [(aa `1),(dom (id (aa `2)))]
.= [(aa `1),(aa `2)]
.= aa by MCART_1:21 ;
then reconsider ii = [(id (aa `1)),(id (aa `2))] as Morphism of a,a by A64, CAT_1:4;
take  ii ; ::_thesis: for b1 being Element of the carrier of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) holds
( ( Hom (a,b1) = {} or for b2 being Morphism of a,b1 holds b2 (*) ii = b2 ) & ( Hom (b1,a) = {} or for b2 being Morphism of b1,a holds ii (*) b2 = b2 ) )
let b be Element of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #); ::_thesis: ( ( Hom (a,b) = {} or for b1 being Morphism of a,b holds b1 (*) ii = b1 ) & ( Hom (b,a) = {} or for b1 being Morphism of b,a holds ii (*) b1 = b1 ) )
thus  ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) ii = g ) ::_thesis: ( Hom (b,a) = {} or for b1 being Morphism of b,a holds ii (*) b1 = b1 )
proof
assume A66: Hom (a,b) <> {} ; ::_thesis: for g being Morphism of a,b holds g (*) ii = g
let g be Morphism of a,b; ::_thesis: g (*) ii = g
reconsider gg = g as Element of [: the carrier' of C, the carrier' of D:] ;
 cod ii = dom g by A66, CAT_1:5, A64;
then A67: [g,ii] in dom |: the Comp of C, the Comp of D:| by A6, CAT_1:def_6;
then A68: dom (gg `1) = cod ([(id (aa `1)),(id (aa `2))] `1) by A4
.= cod (id (aa `1)) ;
A69: the Comp of C . ((gg `1),(id (aa `1))) = (gg `1) (*) (id (aa `1)) by CAT_1:16, A68
.= gg `1 by A68, CAT_1:22 ;
A70: dom (gg `2) = cod ([(id (aa `1)),(id (aa `2))] `2) by A4, A67
.= cod (id (aa `2)) ;
A71: the Comp of D . ((gg `2),(id (aa `2))) = (gg `2) (*) (id (aa `2)) by CAT_1:16, A70
.= gg `2 by A70, CAT_1:22 ;
A72: cod ii = dom g by A64, A66, CAT_1:5;
then  [g,ii] in dom the Comp of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) by A6, CAT_1:def_6;
hence g (*) ii = |: the Comp of C, the Comp of D:| . (g,ii) by CAT_1:def_1
.= [( the Comp of C . ((gg `1),([(id (aa `1)),(id (aa `2))] `1))),( the Comp of D . ((gg `2),([(id (aa `1)),(id (aa `2))] `2)))] by A11, A72
.= g by A69, A71, MCART_1:21 ;
::_thesis: verum
end;
assume A73: Hom (b,a) <> {} ; ::_thesis: for b1 being Morphism of b,a holds ii (*) b1 = b1
let g be Morphism of b,a; ::_thesis: ii (*) g = g
reconsider gg = g as Element of [: the carrier' of C, the carrier' of D:] ;
 dom ii = cod g by A73, CAT_1:5, A65;
then A74: [ii,g] in dom |: the Comp of C, the Comp of D:| by A6, CAT_1:def_6;
then A75: cod (gg `1) = dom ([(id (aa `1)),(id (aa `2))] `1) by A4
.= dom (id (aa `1)) ;
A76: the Comp of C . ((id (aa `1)),(gg `1)) = (id (aa `1)) (*) (gg `1) by CAT_1:16, A75
.= gg `1 by A75, CAT_1:21 ;
A77: cod (gg `2) = dom ([(id (aa `1)),(id (aa `2))] `2) by A4, A74
.= dom (id (aa `2)) ;
A78: the Comp of D . ((id (aa `2)),(gg `2)) = (id (aa `2)) (*) (gg `2) by CAT_1:16, A77
.= gg `2 by A77, CAT_1:21 ;
A79: dom ii = cod g by A65, A73, CAT_1:5;
then  [ii,g] in dom the Comp of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) by A6, CAT_1:def_6;
hence ii (*) g = |: the Comp of C, the Comp of D:| . (ii,g) by CAT_1:def_1
.= [( the Comp of C . (([(id (aa `1)),(id (aa `2))] `1),(gg `1))),( the Comp of D . (([(id (aa `1)),(id (aa `2))] `2),(gg `2)))] by A11, A79
.= g by A76, A78, MCART_1:21 ;
::_thesis: verum
end;
hence  CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) is Category by A6, A32, A35, A62; ::_thesis: verum
end;
end;

:: deftheorem  defines [: CAT_2:def_7_:_
 for C, D being Category holds [:C,D:] = CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #);

theorem :: CAT_2:23
for C, D being Category holds
( the carrier of [:C,D:] = [: the carrier of C, the carrier of D:] & the carrier' of [:C,D:] = [: the carrier' of C, the carrier' of D:] & the Source of [:C,D:] = [: the Source of C, the Source of D:] & the Target of [:C,D:] = [: the Target of C, the Target of D:] & the Comp of [:C,D:] = |: the Comp of C, the Comp of 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:]
proof
thus  [c,d] is Object of [:C,D:] ; ::_thesis: verum
end;
end;

theorem :: CAT_2:24
canceled;

theorem :: CAT_2:25
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:1;

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:]
proof
thus  [f,g] is Morphism of [:C,D:] ; ::_thesis: verum
end;
end;

theorem :: CAT_2:26
canceled;

theorem :: CAT_2:27
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:1;

theorem Th28: :: CAT_2:28
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)] )
proof
let C, D be Category; ::_thesis: 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)] )
let f be Morphism of C; ::_thesis: for g being Morphism of D holds
( dom [f,g] = [(dom f),(dom g)] & cod [f,g] = [(cod f),(cod g)] )
let g be Morphism of D; ::_thesis: ( dom [f,g] = [(dom f),(dom g)] & cod [f,g] = [(cod f),(cod g)] )
thus  dom [f,g] = [: the Source of C, the Source of D:] . (f,g)
.= [(dom f),(dom g)] by FUNCT_3:75 ; ::_thesis: cod [f,g] = [(cod f),(cod g)]
thus  cod [f,g] = [: the Target of C, the Target of D:] . (f,g)
.= [(cod f),(cod g)] by FUNCT_3:75 ; ::_thesis: verum
end;

theorem Th29: :: CAT_2:29
for C, D being Category
for f, f9 being Morphism of C
for g, g9 being Morphism of D st dom f9 = cod f & dom g9 = cod g holds
[f9,g9] (*) [f,g] = [(f9 (*) f),(g9 (*) g)]
proof
let C, D be Category; ::_thesis: for f, f9 being Morphism of C
for g, g9 being Morphism of D st dom f9 = cod f & dom g9 = cod g holds
[f9,g9] (*) [f,g] = [(f9 (*) f),(g9 (*) g)]
let f, f9 be Morphism of C; ::_thesis: for g, g9 being Morphism of D st dom f9 = cod f & dom g9 = cod g holds
[f9,g9] (*) [f,g] = [(f9 (*) f),(g9 (*) g)]
let g, g9 be Morphism of D; ::_thesis: ( dom f9 = cod f & dom g9 = cod g implies [f9,g9] (*) [f,g] = [(f9 (*) f),(g9 (*) g)] )
assume that
A1: dom f9 = cod f and
A2: dom g9 = cod g ; ::_thesis: [f9,g9] (*) [f,g] = [(f9 (*) f),(g9 (*) g)]
A3: ( [f9,f] in dom the Comp of C & [g9,g] in dom the Comp of D ) by A1, A2, CAT_1:15;
 ( dom [f9,g9] = [(dom f9),(dom g9)] & cod [f,g] = [(cod f),(cod g)] ) by Th28;
hence [f9,g9] (*) [f,g] = |: the Comp of C, the Comp of D:| . ([f9,g9],[f,g]) by A1, A2, CAT_1:16
.= [( the Comp of C . (f9,f)),( the Comp of D . (g9,g))] by A3, FUNCT_4:def_3
.= [(f9 (*) f),( the Comp of D . (g9,g))] by A1, CAT_1:16
.= [(f9 (*) f),(g9 (*) g)] by A2, CAT_1:16 ;
::_thesis: verum
end;

theorem Th30: :: CAT_2:30
for C, D being Category
for f, f9 being Morphism of C
for g, g9 being Morphism of D st dom [f9,g9] = cod [f,g] holds
[f9,g9] (*) [f,g] = [(f9 (*) f),(g9 (*) g)]
proof
let C, D be Category; ::_thesis: for f, f9 being Morphism of C
for g, g9 being Morphism of D st dom [f9,g9] = cod [f,g] holds
[f9,g9] (*) [f,g] = [(f9 (*) f),(g9 (*) g)]
let f, f9 be Morphism of C; ::_thesis: for g, g9 being Morphism of D st dom [f9,g9] = cod [f,g] holds
[f9,g9] (*) [f,g] = [(f9 (*) f),(g9 (*) g)]
let g, g9 be Morphism of D; ::_thesis: ( dom [f9,g9] = cod [f,g] implies [f9,g9] (*) [f,g] = [(f9 (*) f),(g9 (*) g)] )
assume A1: dom [f9,g9] = cod [f,g] ; ::_thesis: [f9,g9] (*) [f,g] = [(f9 (*) f),(g9 (*) g)]
 ( [(dom f9),(dom g9)] = dom [f9,g9] & cod [f,g] = [(cod f),(cod g)] ) by Th28;
then  ( dom f9 = cod f & dom g9 = cod g ) by A1, XTUPLE_0:1;
hence  [f9,g9] (*) [f,g] = [(f9 (*) f),(g9 (*) g)] by Th29; ::_thesis: verum
end;

theorem Th31: :: CAT_2:31
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)]
proof
let C, D be Category; ::_thesis: for c being Object of C
for d being Object of D holds id [c,d] = [(id c),(id d)]
let c be Object of C; ::_thesis: for d being Object of D holds id [c,d] = [(id c),(id d)]
let d be Object of D; ::_thesis: id [c,d] = [(id c),(id d)]
A1: dom [(id c),(id d)] = [(dom (id c)),(dom (id d))] by Th28
.= [c,(dom (id d))]
.= [c,d] ;
cod [(id c),(id d)] = [(cod (id c)),(cod (id d))] by Th28
.= [c,(cod (id d))]
.= [c,d] ;
then reconsider m = [(id c),(id d)] as Morphism of [c,d],[c,d] by A1, CAT_1:4;
 for b being Object of [:C,D:] holds
( ( Hom ([c,d],b) <> {} implies for f being Morphism of [c,d],b holds f (*) [(id c),(id d)] = f ) & ( Hom (b,[c,d]) <> {} implies for f being Morphism of b,[c,d] holds [(id c),(id d)] (*) f = f ) )
proof
let b be Object of [:C,D:]; ::_thesis: ( ( Hom ([c,d],b) <> {} implies for f being Morphism of [c,d],b holds f (*) [(id c),(id d)] = f ) & ( Hom (b,[c,d]) <> {} implies for f being Morphism of b,[c,d] holds [(id c),(id d)] (*) f = f ) )
thus  ( Hom ([c,d],b) <> {} implies for f being Morphism of [c,d],b holds f (*) [(id c),(id d)] = f ) ::_thesis: ( Hom (b,[c,d]) <> {} implies for f being Morphism of b,[c,d] holds [(id c),(id d)] (*) f = f )
proof
assume A2: Hom ([c,d],b) <> {} ; ::_thesis: for f being Morphism of [c,d],b holds f (*) [(id c),(id d)] = f
let f be Morphism of [c,d],b; ::_thesis: f (*) [(id c),(id d)] = f
consider fc being Morphism of C, fd being Morphism of D such that
A3: f = [fc,fd] by DOMAIN_1:1;
A4: [c,d] = dom f by A2, CAT_1:5
.= [(dom fc),(dom fd)] by A3, Th28 ;
then A5: c = dom fc by XTUPLE_0:1;
then A6: cod (id c) = dom fc ;
A7: d = dom fd by A4, XTUPLE_0:1;
then  cod (id d) = dom fd ;
hence f (*) [(id c),(id d)] = [(fc (*) (id c)),(fd (*) (id d))] by A3, A6, Th29
.= [fc,(fd (*) (id d))] by A5, CAT_1:22
.= f by A3, A7, CAT_1:22 ;
::_thesis: verum
end;
assume A8: Hom (b,[c,d]) <> {} ; ::_thesis: for f being Morphism of b,[c,d] holds [(id c),(id d)] (*) f = f
let f be Morphism of b,[c,d]; ::_thesis: [(id c),(id d)] (*) f = f
consider fc being Morphism of C, fd being Morphism of D such that
A9: f = [fc,fd] by DOMAIN_1:1;
A10: [c,d] = cod f by A8, CAT_1:5
.= [(cod fc),(cod fd)] by A9, Th28 ;
then A11: c = cod fc by XTUPLE_0:1;
then A12: dom (id c) = cod fc ;
A13: d = cod fd by A10, XTUPLE_0:1;
then  dom (id d) = cod fd ;
hence [(id c),(id d)] (*) f = [((id c) (*) fc),((id d) (*) fd)] by A9, A12, Th29
.= [fc,((id d) (*) fd)] by A11, CAT_1:21
.= f by A9, A13, CAT_1:21 ;
::_thesis: verum
end;
then  m = id [c,d] by CAT_1:def_12;
hence  id [c,d] = [(id c),(id d)] ; ::_thesis: verum
end;

theorem :: CAT_2:32
for C, D being Category
for c, c9 being Object of C
for d, d9 being Object of D holds Hom ([c,d],[c9,d9]) = [:(Hom (c,c9)),(Hom (d,d9)):]
proof
let C, D be Category; ::_thesis: for c, c9 being Object of C
for d, d9 being Object of D holds Hom ([c,d],[c9,d9]) = [:(Hom (c,c9)),(Hom (d,d9)):]
let c, c9 be Object of C; ::_thesis: for d, d9 being Object of D holds Hom ([c,d],[c9,d9]) = [:(Hom (c,c9)),(Hom (d,d9)):]
let d, d9 be Object of D; ::_thesis: Hom ([c,d],[c9,d9]) = [:(Hom (c,c9)),(Hom (d,d9)):]
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_Hom_([c,d],[c9,d9])_implies_x_in_[:(Hom_(c,c9)),(Hom_(d,d9)):]_)_&_(_x_in_[:(Hom_(c,c9)),(Hom_(d,d9)):]_implies_x_in_Hom_([c,d],[c9,d9])_)_)
let x be set ; ::_thesis: ( ( x in Hom ([c,d],[c9,d9]) implies x in [:(Hom (c,c9)),(Hom (d,d9)):] ) & ( x in [:(Hom (c,c9)),(Hom (d,d9)):] implies x in Hom ([c,d],[c9,d9]) ) )
thus  ( x in Hom ([c,d],[c9,d9]) implies x in [:(Hom (c,c9)),(Hom (d,d9)):] ) ::_thesis: ( x in [:(Hom (c,c9)),(Hom (d,d9)):] implies x in Hom ([c,d],[c9,d9]) )
proof
assume A1: x in Hom ([c,d],[c9,d9]) ; ::_thesis: x in [:(Hom (c,c9)),(Hom (d,d9)):]
then reconsider fg = x as Morphism of [c,d],[c9,d9] by CAT_1:def_5;
A2: dom fg = [c,d] by A1, CAT_1:1;
A3: cod fg = [c9,d9] by A1, CAT_1:1;
consider x1, x2 being set  such that
A4: x1 in the carrier' of C and
A5: x2 in the carrier' of D and
A6: fg = [x1,x2] by ZFMISC_1:def_2;
reconsider g = x2 as Morphism of D by A5;
reconsider f = x1 as Morphism of C by A4;
A7: cod fg = [(cod f),(cod g)] by A6, Th28;
then A8: cod f = c9 by A3, XTUPLE_0:1;
A9: cod g = d9 by A3, A7, XTUPLE_0:1;
A10: dom fg = [(dom f),(dom g)] by A6, Th28;
then  dom g = d by A2, XTUPLE_0:1;
then A11: g in Hom (d,d9) by A9;
 dom f = c by A2, A10, XTUPLE_0:1;
then  f in Hom (c,c9) by A8;
hence  x in [:(Hom (c,c9)),(Hom (d,d9)):] by A6, A11, ZFMISC_1:87; ::_thesis: verum
end;
assume  x in [:(Hom (c,c9)),(Hom (d,d9)):] ; ::_thesis: x in Hom ([c,d],[c9,d9])
then consider x1, x2 being set  such that
A12: x1 in Hom (c,c9) and
A13: x2 in Hom (d,d9) and
A14: x = [x1,x2] by ZFMISC_1:def_2;
reconsider g = x2 as Morphism of d,d9 by A13, CAT_1:def_5;
reconsider f = x1 as Morphism of c,c9 by A12, CAT_1:def_5;
 ( cod f = c9 & cod g = d9 ) by A12, A13, CAT_1:1;
then A15: cod [f,g] = [c9,d9] by Th28;
 ( dom f = c & dom g = d ) by A12, A13, CAT_1:1;
then  dom [f,g] = [c,d] by Th28;
hence  x in Hom ([c,d],[c9,d9]) by A14, A15; ::_thesis: verum
end;
hence  Hom ([c,d],[c9,d9]) = [:(Hom (c,c9)),(Hom (d,d9)):] by TARSKI:1; ::_thesis: verum
end;

theorem :: CAT_2:33
for C, D being Category
for c, c9 being Object of C
for f being Morphism of c,c9
for d, d9 being Object of D
for g being Morphism of d,d9 st Hom (c,c9) <> {} & Hom (d,d9) <> {} holds
[f,g] is Morphism of [c,d],[c9,d9]
proof
let C, D be Category; ::_thesis: for c, c9 being Object of C
for f being Morphism of c,c9
for d, d9 being Object of D
for g being Morphism of d,d9 st Hom (c,c9) <> {} & Hom (d,d9) <> {} holds
[f,g] is Morphism of [c,d],[c9,d9]
let c, c9 be Object of C; ::_thesis: for f being Morphism of c,c9
for d, d9 being Object of D
for g being Morphism of d,d9 st Hom (c,c9) <> {} & Hom (d,d9) <> {} holds
[f,g] is Morphism of [c,d],[c9,d9]
let f be Morphism of c,c9; ::_thesis: for d, d9 being Object of D
for g being Morphism of d,d9 st Hom (c,c9) <> {} & Hom (d,d9) <> {} holds
[f,g] is Morphism of [c,d],[c9,d9]
let d, d9 be Object of D; ::_thesis: for g being Morphism of d,d9 st Hom (c,c9) <> {} & Hom (d,d9) <> {} holds
[f,g] is Morphism of [c,d],[c9,d9]
let g be Morphism of d,d9; ::_thesis: ( Hom (c,c9) <> {} & Hom (d,d9) <> {} implies [f,g] is Morphism of [c,d],[c9,d9] )
assume A1: ( Hom (c,c9) <> {} & Hom (d,d9) <> {} ) ; ::_thesis: [f,g] is Morphism of [c,d],[c9,d9]
then  ( cod f = c9 & cod g = d9 ) by CAT_1:5;
then A2: cod [f,g] = [c9,d9] by Th28;
 ( dom f = c & dom g = d ) by A1, CAT_1:5;
then  dom [f,g] = [c,d] by Th28;
hence  [f,g] is Morphism of [c,d],[c9,d9] by A2, CAT_1:4; ::_thesis: verum
end;

definition
let C, C9, D be Category;
let S be Functor of [:C,C9:],D;
let m be Morphism of C;
let m9 be Morphism of C9;
:: original: .
redefine funcS . (m,m9) ->  Morphism of D;
coherence
 S . (m,m9) is Morphism of D
proof
 S . (m,m9) = S . [m,m9] ;
hence  S . (m,m9) is Morphism of D ; ::_thesis: verum
end;
end;

theorem Th34: :: CAT_2:34
for C, C9, D being Category
for S being Functor of [:C,C9:],D
for c being Object of C holds (curry S) . (id c) is Functor of C9,D
proof
let C, C9, D be Category; ::_thesis: for S being Functor of [:C,C9:],D
for c being Object of C holds (curry S) . (id c) is Functor of C9,D
let S be Functor of [:C,C9:],D; ::_thesis: for c being Object of C holds (curry S) . (id c) is Functor of C9,D
let c be Object of C; ::_thesis: (curry S) . (id c) is Functor of C9,D
reconsider S9 = S as Function of [: the carrier' of C, the carrier' of C9:], the carrier' of D ;
reconsider T = (curry S9) . (id c) as Function of the carrier' of C9, the carrier' of D ;
now__::_thesis:_(_(_for_c9_being_Object_of_C9_ex_d_being_Object_of_D_st_T_._(id_c9)_=_id_d_)_&_(_for_f_being_Morphism_of_C9_holds_
(_T_._(id_(dom_f))_=_id_(dom_(T_._f))_&_T_._(id_(cod_f))_=_id_(cod_(T_._f))_)_)_&_(_for_f,_g_being_Morphism_of_C9_st_dom_g_=_cod_f_holds_
T_._(g_(*)_f)_=_(T_._g)_(*)_(T_._f)_)_)
thus  for c9 being Object of C9 ex d being Object of D st T . (id c9) = id d ::_thesis: ( ( for f being Morphism of C9 holds
( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) ) ) & ( for f, g being Morphism of C9 st dom g = cod f holds
T . (g (*) f) = (T . g) (*) (T . f) ) )
proof
let c9 be Object of C9; ::_thesis: ex d being Object of D st T . (id c9) = id d
consider d being Object of D such that
A1: S . (id [c,c9]) = id d by CAT_1:62;
take  d ; ::_thesis: T . (id c9) = id d
thus T . (id c9) = S . ((id c),(id c9)) by FUNCT_5:69
.= id d by A1, Th31 ; ::_thesis: verum
end;
A2: ( dom (id c) = c & cod (id c) = c ) ;
thus  for f being Morphism of C9 holds
( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) ) ::_thesis: for f, g being Morphism of C9 st dom g = cod f holds
T . (g (*) f) = (T . g) (*) (T . f)
proof
let f be Morphism of C9; ::_thesis: ( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) )
thus T . (id (dom f)) = S . ((id c),(id (dom f))) by FUNCT_5:69
.= S . (id [c,(dom f)]) by Th31
.= S . (id [(dom (id c)),(dom f)])
.= S . (id (dom [(id c),f])) by Th28
.= id (dom (S . ((id c),f))) by CAT_1:63
.= id (dom (T . f)) by FUNCT_5:69 ; ::_thesis: T . (id (cod f)) = id (cod (T . f))
thus T . (id (cod f)) = S . ((id c),(id (cod f))) by FUNCT_5:69
.= S . (id [c,(cod f)]) by Th31
.= S . (id [(cod (id c)),(cod f)])
.= S . (id (cod [(id c),f])) by Th28
.= id (cod (S . ((id c),f))) by CAT_1:63
.= id (cod (T . f)) by FUNCT_5:69 ; ::_thesis: verum
end;
let f, g be Morphism of C9; ::_thesis: ( dom g = cod f implies T . (g (*) f) = (T . g) (*) (T . f) )
assume A3: dom g = cod f ; ::_thesis: T . (g (*) f) = (T . g) (*) (T . f)
 Hom (c,c) <> {} ;
then A4: (id c) * (id c) = (id c) (*) (id c) by CAT_1:def_13;
A5: ( dom [(id c),g] = [(dom (id c)),(dom g)] & cod [(id c),f] = [(cod (id c)),(cod f)] ) by Th28;
thus T . (g (*) f) = S . (((id c) * (id c)),(g (*) f)) by FUNCT_5:69
.= S . ([(id c),g] (*) [(id c),f]) by A3, A2, A4, Th29
.= (S . ((id c),g)) (*) (S . ((id c),f)) by A3, A5, CAT_1:64
.= (T . g) (*) (S . ((id c),f)) by FUNCT_5:69
.= (T . g) (*) (T . f) by FUNCT_5:69 ; ::_thesis: verum
end;
hence  (curry S) . (id c) is Functor of C9,D by CAT_1:61; ::_thesis: verum
end;

theorem Th35: :: CAT_2:35
for C, C9, D being Category
for S being Functor of [:C,C9:],D
for c9 being Object of C9 holds (curry' S) . (id c9) is Functor of C,D
proof
let C, C9, D be Category; ::_thesis: for S being Functor of [:C,C9:],D
for c9 being Object of C9 holds (curry' S) . (id c9) is Functor of C,D
let S be Functor of [:C,C9:],D; ::_thesis: for c9 being Object of C9 holds (curry' S) . (id c9) is Functor of C,D
let c9 be Object of C9; ::_thesis: (curry' S) . (id c9) is Functor of C,D
reconsider S9 = S as Function of [: the carrier' of C, the carrier' of C9:], the carrier' of D ;
reconsider T = (curry' S9) . (id c9) as Function of the carrier' of C, the carrier' of D ;
now__::_thesis:_(_(_for_c_being_Object_of_C_ex_d_being_Object_of_D_st_T_._(id_c)_=_id_d_)_&_(_for_f_being_Morphism_of_C_holds_
(_T_._(id_(dom_f))_=_id_(dom_(T_._f))_&_T_._(id_(cod_f))_=_id_(cod_(T_._f))_)_)_&_(_for_f,_g_being_Morphism_of_C_st_dom_g_=_cod_f_holds_
T_._(g_(*)_f)_=_(T_._g)_(*)_(T_._f)_)_)
thus  for c being Object of C ex d being Object of D st T . (id c) = id d ::_thesis: ( ( for f being Morphism of C holds
( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds
T . (g (*) f) = (T . g) (*) (T . f) ) )
proof
let c be Object of C; ::_thesis: ex d being Object of D st T . (id c) = id d
consider d being Object of D such that
A1: S . (id [c,c9]) = id d by CAT_1:62;
take  d ; ::_thesis: T . (id c) = id d
thus T . (id c) = S . ((id c),(id c9)) by FUNCT_5:70
.= id d by A1, Th31 ; ::_thesis: verum
end;
A2: ( dom (id c9) = c9 & cod (id c9) = c9 ) ;
thus  for f being Morphism of C holds
( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) ) ::_thesis: for f, g being Morphism of C st dom g = cod f holds
T . (g (*) f) = (T . g) (*) (T . f)
proof
let f be Morphism of C; ::_thesis: ( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) )
thus T . (id (dom f)) = S . ((id (dom f)),(id c9)) by FUNCT_5:70
.= S . (id [(dom f),c9]) by Th31
.= S . (id [(dom f),(dom (id c9))])
.= S . (id (dom [f,(id c9)])) by Th28
.= id (dom (S . (f,(id c9)))) by CAT_1:63
.= id (dom (T . f)) by FUNCT_5:70 ; ::_thesis: T . (id (cod f)) = id (cod (T . f))
thus T . (id (cod f)) = S . ((id (cod f)),(id c9)) by FUNCT_5:70
.= S . (id [(cod f),c9]) by Th31
.= S . (id [(cod f),(cod (id c9))])
.= S . (id (cod [f,(id c9)])) by Th28
.= id (cod (S . (f,(id c9)))) by CAT_1:63
.= id (cod (T . f)) by FUNCT_5:70 ; ::_thesis: verum
end;
let f, g be Morphism of C; ::_thesis: ( dom g = cod f implies T . (g (*) f) = (T . g) (*) (T . f) )
assume A3: dom g = cod f ; ::_thesis: T . (g (*) f) = (T . g) (*) (T . f)
 Hom (c9,c9) <> {} ;
then A4: (id c9) * (id c9) = (id c9) (*) (id c9) by CAT_1:def_13;
A5: ( dom [g,(id c9)] = [(dom g),(dom (id c9))] & cod [f,(id c9)] = [(cod f),(cod (id c9))] ) by Th28;
thus T . (g (*) f) = S . ((g (*) f),((id c9) * (id c9))) by FUNCT_5:70
.= S . ([g,(id c9)] (*) [f,(id c9)]) by A3, A2, A4, Th29
.= (S . (g,(id c9))) (*) (S . (f,(id c9))) by A3, A5, CAT_1:64
.= (T . g) (*) (S . (f,(id c9))) by FUNCT_5:70
.= (T . g) (*) (T . f) by FUNCT_5:70 ; ::_thesis: verum
end;
hence  (curry' S) . (id c9) is Functor of C,D by CAT_1:61; ::_thesis: verum
end;

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

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

theorem :: CAT_2:36
for C, C9, D being Category
for S being Functor of [:C,C9:],D
for c being Object of C
for f being Morphism of C9 holds (S ?- c) . f = S . ((id c),f) by FUNCT_5:69;

theorem :: CAT_2:37
for C, C9, D being Category
for S being Functor of [:C,C9:],D
for c being Object of C
for c9 being Object of C9 holds (Obj (S ?- c)) . c9 = (Obj S) . (c,c9)
proof
let C, C9, D be Category; ::_thesis: for S being Functor of [:C,C9:],D
for c being Object of C
for c9 being Object of C9 holds (Obj (S ?- c)) . c9 = (Obj S) . (c,c9)
let S be Functor of [:C,C9:],D; ::_thesis: for c being Object of C
for c9 being Object of C9 holds (Obj (S ?- c)) . c9 = (Obj S) . (c,c9)
let c be Object of C; ::_thesis: for c9 being Object of C9 holds (Obj (S ?- c)) . c9 = (Obj S) . (c,c9)
let c9 be Object of C9; ::_thesis: (Obj (S ?- c)) . c9 = (Obj S) . (c,c9)
(S ?- c) . (id c9) = S . ((id c),(id c9)) by FUNCT_5:69
.= S . (id [c,c9]) by Th31
.= id ((Obj S) . [c,c9]) by CAT_1:68 ;
hence  (Obj (S ?- c)) . c9 = (Obj S) . (c,c9) by CAT_1:67; ::_thesis: verum
end;

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

:: deftheorem  defines -? CAT_2:def_9_:_
 for C, C9, D being Category
for S being Functor of [:C,C9:],D
for c9 being Object of C9 holds S -? c9 = (curry' S) . (id c9);

theorem :: CAT_2:38
for C, C9, D being Category
for S being Functor of [:C,C9:],D
for c9 being Object of C9
for f being Morphism of C holds (S -? c9) . f = S . (f,(id c9)) by FUNCT_5:70;

theorem :: CAT_2:39
for C, C9, D being Category
for S being Functor of [:C,C9:],D
for c being Object of C
for c9 being Object of C9 holds (Obj (S -? c9)) . c = (Obj S) . (c,c9)
proof
let C, C9, D be Category; ::_thesis: for S being Functor of [:C,C9:],D
for c being Object of C
for c9 being Object of C9 holds (Obj (S -? c9)) . c = (Obj S) . (c,c9)
let S be Functor of [:C,C9:],D; ::_thesis: for c being Object of C
for c9 being Object of C9 holds (Obj (S -? c9)) . c = (Obj S) . (c,c9)
let c be Object of C; ::_thesis: for c9 being Object of C9 holds (Obj (S -? c9)) . c = (Obj S) . (c,c9)
let c9 be Object of C9; ::_thesis: (Obj (S -? c9)) . c = (Obj S) . (c,c9)
(S -? c9) . (id c) = S . ((id c),(id c9)) by FUNCT_5:70
.= S . (id [c,c9]) by Th31
.= id ((Obj S) . [c,c9]) by CAT_1:68 ;
hence  (Obj (S -? c9)) . c = (Obj S) . (c,c9) by CAT_1:67; ::_thesis: verum
end;

theorem :: CAT_2:40
for C, B, D being Category
for L being Function of the carrier of C,(Funct (B,D))
for M being Function of the carrier 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
let C, B, D be Category; ::_thesis: for L being Function of the carrier of C,(Funct (B,D))
for M being Function of the carrier 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)
deffunc H1( Category) ->  set = the carrier' of $1;
let L be Function of the carrier of C,(Funct (B,D)); ::_thesis: for M being Function of the carrier 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)
let M be Function of the carrier of B,(Funct (C,D)); ::_thesis: ( ( 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) ) implies 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) )
assume that
A1: for c being Object of C
for b being Object of B holds (M . b) . (id c) = (L . c) . (id b) and
A2: 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) ; ::_thesis: 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)
deffunc H2( Element of H1(B), Element of H1(C)) ->  Element of the carrier' of D = ((L . (cod $2)) . $1) (*) ((M . (dom $1)) . $2);
consider S being Function of [:H1(B),H1(C):],H1(D) such that
A3: for f being Morphism of B
for g being Morphism of C holds S . (f,g) = H2(f,g) from BINOP_1:sch_4();
reconsider T = S as Function of H1([:B,C:]),H1(D) ;
now__::_thesis:_(_(_for_bc_being_Object_of_[:B,C:]_ex_d_being_Object_of_D_st_T_._(id_bc)_=_id_d_)_&_(_for_fg_being_Morphism_of_[:B,C:]_holds_
(_T_._(id_(dom_fg))_=_id_(dom_(T_._fg))_&_T_._(id_(cod_fg))_=_id_(cod_(T_._fg))_)_)_&_(_for_fg1,_fg2_being_Morphism_of_[:B,C:]_st_dom_fg2_=_cod_fg1_holds_
T_._(fg2_(*)_fg1)_=_(T_._fg2)_(*)_(T_._fg1)_)_)
thus  for bc being Object of [:B,C:] ex d being Object of D st T . (id bc) = id d ::_thesis: ( ( for fg being Morphism of [:B,C:] holds
( T . (id (dom fg)) = id (dom (T . fg)) & T . (id (cod fg)) = id (cod (T . fg)) ) ) & ( for fg1, fg2 being Morphism of [:B,C:] st dom fg2 = cod fg1 holds
T . (fg2 (*) fg1) = (T . fg2) (*) (T . fg1) ) )
proof
let bc be Object of [:B,C:]; ::_thesis: ex d being Object of D st T . (id bc) = id d
consider b being Object of B, c being Object of C such that
A4: bc = [b,c] by DOMAIN_1:1;
consider d being Object of D such that
A5: (L . c) . (id b) = id d by CAT_1:62;
take  d ; ::_thesis: T . (id bc) = id d
 Hom (d,d) <> {} ;
then A6: (id d) * (id d) = (id d) (*) (id d) by CAT_1:def_13;
A7: ( cod (id c) = c & dom (id b) = b ) ;
 (L . c) . (id b) = (M . b) . (id c) by A1;
then  T . ((id b),(id c)) = id d by A3, A5, A6, A7;
hence  T . (id bc) = id d by A4, Th31; ::_thesis: verum
end;
thus  for fg being Morphism of [:B,C:] holds
( T . (id (dom fg)) = id (dom (T . fg)) & T . (id (cod fg)) = id (cod (T . fg)) ) ::_thesis: for fg1, fg2 being Morphism of [:B,C:] st dom fg2 = cod fg1 holds
T . (fg2 (*) fg1) = (T . fg2) (*) (T . fg1)
proof
let fg be Morphism of [:B,C:]; ::_thesis: ( T . (id (dom fg)) = id (dom (T . fg)) & T . (id (cod fg)) = id (cod (T . fg)) )
consider f being Morphism of B, g being Morphism of C such that
A8: fg = [f,g] by DOMAIN_1:1;
set b = dom f;
set c = dom g;
set g9 = id (dom g);
set f9 = id (dom f);
A9: Hom ((dom ((M . (dom f)) . g)),(dom ((M . (dom f)) . g))) <> {} ;
id (dom ((L . (cod g)) . f)) = (L . (cod g)) . (id (dom f)) by CAT_1:63
.= (M . (dom f)) . (id (cod g)) by A1
.= id (cod ((M . (dom f)) . g)) by CAT_1:63 ;
then A10: dom ((L . (cod g)) . f) = cod ((M . (dom f)) . g) by CAT_1:59;
thus T . (id (dom fg)) = S . (id [(dom f),(dom g)]) by A8, Th28
.= S . ((id (dom f)),(id (dom g))) by Th31
.= ((L . (cod (id (dom g)))) . (id (dom f))) (*) ((M . (dom (id (dom f)))) . (id (dom g))) by A3
.= ((L . (dom g)) . (id (dom f))) (*) ((M . (dom (id (dom f)))) . (id (dom g)))
.= ((L . (dom g)) . (id (dom f))) (*) ((M . (dom f)) . (id (dom g)))
.= ((M . (dom f)) . (id (dom g))) (*) ((M . (dom f)) . (id (dom g))) by A1
.= (id (dom ((M . (dom f)) . g))) (*) ((M . (dom f)) . (id (dom g))) by CAT_1:63
.= (id (dom ((M . (dom f)) . g))) (*) (id (dom ((M . (dom f)) . g))) by CAT_1:63
.= (id (dom ((M . (dom f)) . g))) * (id (dom ((M . (dom f)) . g))) by A9, CAT_1:def_13
.= id (dom (((L . (cod g)) . f) (*) ((M . (dom f)) . g))) by A10, CAT_1:17
.= id (dom (S . (f,g))) by A3
.= id (dom (T . fg)) by A8 ; ::_thesis: T . (id (cod fg)) = id (cod (T . fg))
set b = cod f;
set c = cod g;
set g9 = id (cod g);
set f9 = id (cod f);
A11: Hom ((cod ((L . (cod g)) . f)),(cod ((L . (cod g)) . f))) <> {} ;
thus T . (id (cod fg)) = S . (id [(cod f),(cod g)]) by A8, Th28
.= S . ((id (cod f)),(id (cod g))) by Th31
.= ((L . (cod (id (cod g)))) . (id (cod f))) (*) ((M . (dom (id (cod f)))) . (id (cod g))) by A3
.= ((L . (cod g)) . (id (cod f))) (*) ((M . (dom (id (cod f)))) . (id (cod g)))
.= ((L . (cod g)) . (id (cod f))) (*) ((M . (cod f)) . (id (cod g)))
.= ((L . (cod g)) . (id (cod f))) (*) ((L . (cod g)) . (id (cod f))) by A1
.= (id (cod ((L . (cod g)) . f))) (*) ((L . (cod g)) . (id (cod f))) by CAT_1:63
.= (id (cod ((L . (cod g)) . f))) (*) (id (cod ((L . (cod g)) . f))) by CAT_1:63
.= (id (cod ((L . (cod g)) . f))) * (id (cod ((L . (cod g)) . f))) by A11, CAT_1:def_13
.= id (cod (((L . (cod g)) . f) (*) ((M . (dom f)) . g))) by A10, CAT_1:17
.= id (cod (S . (f,g))) by A3
.= id (cod (T . fg)) by A8 ; ::_thesis: verum
end;
let fg1, fg2 be Morphism of [:B,C:]; ::_thesis: ( dom fg2 = cod fg1 implies T . (fg2 (*) fg1) = (T . fg2) (*) (T . fg1) )
assume A12: dom fg2 = cod fg1 ; ::_thesis: T . (fg2 (*) fg1) = (T . fg2) (*) (T . fg1)
consider f1 being Morphism of B, g1 being Morphism of C such that
A13: fg1 = [f1,g1] by DOMAIN_1:1;
consider f2 being Morphism of B, g2 being Morphism of C such that
A14: fg2 = [f2,g2] by DOMAIN_1:1;
A15: [(cod f1),(cod g1)] = cod fg1 by A13, Th28;
set L1 = L . (cod g1);
set L2 = L . (cod g2);
set M1 = M . (dom f1);
set M2 = M . (dom f2);
A16: [(dom f2),(dom g2)] = dom fg2 by A14, Th28;
then A17: dom f2 = cod f1 by A12, A15, XTUPLE_0:1;
then A18: dom ((L . (cod g2)) . f2) = cod ((L . (cod g2)) . f1) by CAT_1:64;
id (dom ((L . (cod g1)) . f1)) = (L . (cod g1)) . (id (dom f1)) by CAT_1:63
.= (M . (dom f1)) . (id (cod g1)) by A1
.= id (cod ((M . (dom f1)) . g1)) by CAT_1:63 ;
then A19: dom ((L . (cod g1)) . f1) = cod ((M . (dom f1)) . g1) by CAT_1:59;
then A20: cod (((L . (cod g1)) . f1) (*) ((M . (dom f1)) . g1)) = cod ((L . (cod g1)) . f1) by CAT_1:17;
A21: dom g2 = cod g1 by A12, A16, A15, XTUPLE_0:1;
then A22: dom ((M . (dom f1)) . g2) = cod ((M . (dom f1)) . g1) by CAT_1:64;
then A23: cod (((M . (dom f1)) . g2) (*) ((M . (dom f1)) . g1)) = cod ((M . (dom f1)) . g2) by CAT_1:17;
id (dom ((M . (dom f2)) . g2)) = (M . (dom f2)) . (id (dom g2)) by CAT_1:63
.= (L . (cod g1)) . (id (cod f1)) by A1, A17, A21
.= id (cod ((L . (cod g1)) . f1)) by CAT_1:63 ;
then A24: dom ((M . (dom f2)) . g2) = cod ((L . (cod g1)) . f1) by CAT_1:59;
id (dom ((L . (cod g2)) . f2)) = (L . (cod g2)) . (id (dom f2)) by CAT_1:63
.= (M . (dom f2)) . (id (cod g2)) by A1
.= id (cod ((M . (dom f2)) . g2)) by CAT_1:63 ;
then A25: dom ((L . (cod g2)) . f2) = cod ((M . (dom f2)) . g2) by CAT_1:59;
set f = f2 (*) f1;
set g = g2 (*) g1;
id (dom ((L . (cod g2)) . f1)) = (L . (cod g2)) . (id (dom f1)) by CAT_1:63
.= (M . (dom f1)) . (id (cod g2)) by A1
.= id (cod ((M . (dom f1)) . g2)) by CAT_1:63 ;
then A26: dom ((L . (cod g2)) . f1) = cod ((M . (dom f1)) . g2) by CAT_1:59;
thus T . (fg2 (*) fg1) = S . ((f2 (*) f1),(g2 (*) g1)) by A12, A13, A14, Th30
.= ((L . (cod (g2 (*) g1))) . (f2 (*) f1)) (*) ((M . (dom (f2 (*) f1))) . (g2 (*) g1)) by A3
.= ((L . (cod g2)) . (f2 (*) f1)) (*) ((M . (dom (f2 (*) f1))) . (g2 (*) g1)) by A21, CAT_1:17
.= ((L . (cod g2)) . (f2 (*) f1)) (*) ((M . (dom f1)) . (g2 (*) g1)) by A17, CAT_1:17
.= (((L . (cod g2)) . f2) (*) ((L . (cod g2)) . f1)) (*) ((M . (dom f1)) . (g2 (*) g1)) by A17, CAT_1:64
.= (((L . (cod g2)) . f2) (*) ((L . (cod g2)) . f1)) (*) (((M . (dom f1)) . g2) (*) ((M . (dom f1)) . g1)) by A21, CAT_1:64
.= ((L . (cod g2)) . f2) (*) (((L . (cod g2)) . f1) (*) (((M . (dom f1)) . g2) (*) ((M . (dom f1)) . g1))) by A18, A23, A26, CAT_1:18
.= ((L . (cod g2)) . f2) (*) ((((L . (cod g2)) . f1) (*) ((M . (dom f1)) . g2)) (*) ((M . (dom f1)) . g1)) by A22, A26, CAT_1:18
.= ((L . (cod g2)) . f2) (*) ((((M . (dom f2)) . g2) (*) ((L . (cod g1)) . f1)) (*) ((M . (dom f1)) . g1)) by A2, A17, A21
.= ((L . (cod g2)) . f2) (*) (((M . (dom f2)) . g2) (*) (((L . (cod g1)) . f1) (*) ((M . (dom f1)) . g1))) by A19, A24, CAT_1:18
.= (((L . (cod g2)) . f2) (*) ((M . (dom f2)) . g2)) (*) (((L . (cod g1)) . f1) (*) ((M . (dom f1)) . g1)) by A24, A25, A20, CAT_1:18
.= (((L . (cod g2)) . f2) (*) ((M . (dom f2)) . g2)) (*) (S . (f1,g1)) by A3
.= (S . (f2,g2)) (*) (T . fg1) by A3, A13
.= (T . fg2) (*) (T . fg1) by A14 ; ::_thesis: verum
end;
then reconsider T = T as Functor of [:B,C:],D by CAT_1:61;
take  T ; ::_thesis: for f being Morphism of B
for g being Morphism of C holds T . (f,g) = ((L . (cod g)) . f) (*) ((M . (dom f)) . g)
thus  for f being Morphism of B
for g being Morphism of C holds T . (f,g) = ((L . (cod g)) . f) (*) ((M . (dom f)) . g) by A3; ::_thesis: verum
end;

theorem :: CAT_2:41
for C, B, D being Category
for L being Function of the carrier of C,(Funct (B,D))
for M being Function of the carrier 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
let C, B, D be Category; ::_thesis: for L being Function of the carrier of C,(Funct (B,D))
for M being Function of the carrier 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)
let L be Function of the carrier of C,(Funct (B,D)); ::_thesis: for M being Function of the carrier 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)
let M be Function of the carrier of B,(Funct (C,D)); ::_thesis: ( 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 ) implies 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) )
given S being Functor of [:B,C:],D such that A1: for c being Object of C
for b being Object of B holds
( S -? c = L . c & S ?- b = M . b ) ; ::_thesis: 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)
let f be Morphism of B; ::_thesis: for g being Morphism of C holds ((M . (cod f)) . g) (*) ((L . (dom g)) . f) = ((L . (cod g)) . f) (*) ((M . (dom f)) . g)
let g be Morphism of C; ::_thesis: ((M . (cod f)) . g) (*) ((L . (dom g)) . f) = ((L . (cod g)) . f) (*) ((M . (dom f)) . g)
 dom (id (cod f)) = cod f ;
then A2: dom [(id (cod f)),g] = [(cod f),(dom g)] by Th28;
 cod (id (dom g)) = dom g ;
then A3: cod [f,(id (dom g))] = [(cod f),(dom g)] by Th28;
 cod (id (dom f)) = dom f ;
then A4: cod [(id (dom f)),g] = [(dom f),(cod g)] by Th28;
 dom (id (cod g)) = cod g ;
then A5: dom [f,(id (cod g))] = [(dom f),(cod g)] by Th28;
thus ((M . (cod f)) . g) (*) ((L . (dom g)) . f) = ((S ?- (cod f)) . g) (*) ((L . (dom g)) . f) by A1
.= ((S ?- (cod f)) . g) (*) ((S -? (dom g)) . f) by A1
.= (S . ((id (cod f)),g)) (*) ((S -? (dom g)) . f) by FUNCT_5:69
.= (S . ((id (cod f)),g)) (*) (S . (f,(id (dom g)))) by FUNCT_5:70
.= S . ([(id (cod f)),g] (*) [f,(id (dom g))]) by A2, A3, CAT_1:64
.= S . [((id (cod f)) (*) f),(g (*) (id (dom g)))] by A2, A3, Th30
.= S . [f,(g (*) (id (dom g)))] by CAT_1:21
.= S . [f,g] by CAT_1:22
.= S . [(f (*) (id (dom f))),g] by CAT_1:22
.= S . [(f (*) (id (dom f))),((id (cod g)) (*) g)] by CAT_1:21
.= S . ([f,(id (cod g))] (*) [(id (dom f)),g]) by A5, A4, Th30
.= (S . (f,(id (cod g)))) (*) (S . [(id (dom f)),g]) by A5, A4, CAT_1:64
.= ((S -? (cod g)) . f) (*) (S . ((id (dom f)),g)) by FUNCT_5:70
.= ((S -? (cod g)) . f) (*) ((S ?- (dom f)) . g) by FUNCT_5:69
.= ((L . (cod g)) . f) (*) ((S ?- (dom f)) . g) by A1
.= ((L . (cod g)) . f) (*) ((M . (dom f)) . g) by A1 ; ::_thesis: verum
end;

definition
let C, D be Category;
func pr1 (C,D) ->  Functor of [:C,D:],C equals :: CAT_2:def 10
 pr1 ( the carrier' of C, the carrier' of D);
coherence
 pr1 ( the carrier' of C, the carrier' of D) is Functor of [:C,D:],C
proof
reconsider T = pr1 ( the carrier' of C, the carrier' of D) as Function of the carrier' of [:C,D:], the carrier' of C ;
now__::_thesis:_(_(_for_cd_being_Object_of_[:C,D:]_ex_c_being_Object_of_C_st_T_._(id_cd)_=_id_c_)_&_(_for_fg_being_Morphism_of_[:C,D:]_holds_
(_T_._(id_(dom_fg))_=_id_(dom_(T_._fg))_&_T_._(id_(cod_fg))_=_id_(cod_(T_._fg))_)_)_&_(_for_fg,_fg9_being_Morphism_of_[:C,D:]_st_dom_fg9_=_cod_fg_holds_
T_._(fg9_(*)_fg)_=_(T_._fg9)_(*)_(T_._fg)_)_)
thus  for cd being Object of [:C,D:] ex c being Object of C st T . (id cd) = id c ::_thesis: ( ( for fg being Morphism of [:C,D:] holds
( T . (id (dom fg)) = id (dom (T . fg)) & T . (id (cod fg)) = id (cod (T . fg)) ) ) & ( for fg, fg9 being Morphism of [:C,D:] st dom fg9 = cod fg holds
T . (fg9 (*) fg) = (T . fg9) (*) (T . fg) ) )
proof
let cd be Object of [:C,D:]; ::_thesis: ex c being Object of C st T . (id cd) = id c
consider c being Object of C, d being Object of D such that
A1: cd = [c,d] by DOMAIN_1:1;
A2: T . ((id c),(id d)) = id c by FUNCT_3:def_4;
 id cd = [(id c),(id d)] by A1, Th31;
hence  ex c being Object of C st T . (id cd) = id c by A2; ::_thesis: verum
end;
thus  for fg being Morphism of [:C,D:] holds
( T . (id (dom fg)) = id (dom (T . fg)) & T . (id (cod fg)) = id (cod (T . fg)) ) ::_thesis: for fg, fg9 being Morphism of [:C,D:] st dom fg9 = cod fg holds
T . (fg9 (*) fg) = (T . fg9) (*) (T . fg)
proof
let fg be Morphism of [:C,D:]; ::_thesis: ( T . (id (dom fg)) = id (dom (T . fg)) & T . (id (cod fg)) = id (cod (T . fg)) )
consider f being Morphism of C, g being Morphism of D such that
A3: fg = [f,g] by DOMAIN_1:1;
 T . (f,g) = T . fg by A3;
then A4: T . fg = f by FUNCT_3:def_4;
 dom [f,g] = [(dom f),(dom g)] by Th28;
hence T . (id (dom fg)) = T . ((id (dom f)),(id (dom g))) by A3, Th31
.= id (dom (T . fg)) by A4, FUNCT_3:def_4 ;
::_thesis: T . (id (cod fg)) = id (cod (T . fg))
 cod [f,g] = [(cod f),(cod g)] by Th28;
hence T . (id (cod fg)) = T . ((id (cod f)),(id (cod g))) by A3, Th31
.= id (cod (T . fg)) by A4, FUNCT_3:def_4 ;
::_thesis: verum
end;
let fg, fg9 be Morphism of [:C,D:]; ::_thesis: ( dom fg9 = cod fg implies T . (fg9 (*) fg) = (T . fg9) (*) (T . fg) )
assume A5: dom fg9 = cod fg ; ::_thesis: T . (fg9 (*) fg) = (T . fg9) (*) (T . fg)
consider f being Morphism of C, g being Morphism of D such that
A6: fg = [f,g] by DOMAIN_1:1;
 T . (f,g) = T . fg by A6;
then A7: T . fg = f by FUNCT_3:def_4;
consider f9 being Morphism of C, g9 being Morphism of D such that
A8: fg9 = [f9,g9] by DOMAIN_1:1;
 T . (f9,g9) = T . fg9 by A8;
then A9: T . fg9 = f9 by FUNCT_3:def_4;
 ( dom [f9,g9] = [(dom f9),(dom g9)] & cod [f,g] = [(cod f),(cod g)] ) by Th28;
then  ( dom f9 = cod f & dom g9 = cod g ) by A5, A6, A8, XTUPLE_0:1;
hence T . (fg9 (*) fg) = T . ((f9 (*) f),(g9 (*) g)) by A6, A8, Th29
.= (T . fg9) (*) (T . fg) by A9, A7, FUNCT_3:def_4 ;
::_thesis: verum
end;
hence  pr1 ( the carrier' of C, the carrier' of D) is Functor of [:C,D:],C by CAT_1:61; ::_thesis: verum
end;
func pr2 (C,D) ->  Functor of [:C,D:],D equals :: CAT_2:def 11
 pr2 ( the carrier' of C, the carrier' of D);
coherence
 pr2 ( the carrier' of C, the carrier' of D) is Functor of [:C,D:],D
proof
reconsider T = pr2 ( the carrier' of C, the carrier' of D) as Function of the carrier' of [:C,D:], the carrier' of D ;
now__::_thesis:_(_(_for_cd_being_Object_of_[:C,D:]_ex_d_being_Object_of_D_st_T_._(id_cd)_=_id_d_)_&_(_for_fg_being_Morphism_of_[:C,D:]_holds_
(_T_._(id_(dom_fg))_=_id_(dom_(T_._fg))_&_T_._(id_(cod_fg))_=_id_(cod_(T_._fg))_)_)_&_(_for_fg,_fg9_being_Morphism_of_[:C,D:]_st_dom_fg9_=_cod_fg_holds_
T_._(fg9_(*)_fg)_=_(T_._fg9)_(*)_(T_._fg)_)_)
thus  for cd being Object of [:C,D:] ex d being Object of D st T . (id cd) = id d ::_thesis: ( ( for fg being Morphism of [:C,D:] holds
( T . (id (dom fg)) = id (dom (T . fg)) & T . (id (cod fg)) = id (cod (T . fg)) ) ) & ( for fg, fg9 being Morphism of [:C,D:] st dom fg9 = cod fg holds
T . (fg9 (*) fg) = (T . fg9) (*) (T . fg) ) )
proof
let cd be Object of [:C,D:]; ::_thesis: ex d being Object of D st T . (id cd) = id d
consider c being Object of C, d being Object of D such that
A10: cd = [c,d] by DOMAIN_1:1;
A11: T . ((id c),(id d)) = id d by FUNCT_3:def_5;
 id cd = [(id c),(id d)] by A10, Th31;
hence  ex d being Object of D st T . (id cd) = id d by A11; ::_thesis: verum
end;
thus  for fg being Morphism of [:C,D:] holds
( T . (id (dom fg)) = id (dom (T . fg)) & T . (id (cod fg)) = id (cod (T . fg)) ) ::_thesis: for fg, fg9 being Morphism of [:C,D:] st dom fg9 = cod fg holds
T . (fg9 (*) fg) = (T . fg9) (*) (T . fg)
proof
let fg be Morphism of [:C,D:]; ::_thesis: ( T . (id (dom fg)) = id (dom (T . fg)) & T . (id (cod fg)) = id (cod (T . fg)) )
consider f being Morphism of C, g being Morphism of D such that
A12: fg = [f,g] by DOMAIN_1:1;
 T . (f,g) = T . fg by A12;
then A13: T . fg = g by FUNCT_3:def_5;
 dom [f,g] = [(dom f),(dom g)] by Th28;
hence T . (id (dom fg)) = T . ((id (dom f)),(id (dom g))) by A12, Th31
.= id (dom (T . fg)) by A13, FUNCT_3:def_5 ;
::_thesis: T . (id (cod fg)) = id (cod (T . fg))
 cod [f,g] = [(cod f),(cod g)] by Th28;
hence T . (id (cod fg)) = T . ((id (cod f)),(id (cod g))) by A12, Th31
.= id (cod (T . fg)) by A13, FUNCT_3:def_5 ;
::_thesis: verum
end;
let fg, fg9 be Morphism of [:C,D:]; ::_thesis: ( dom fg9 = cod fg implies T . (fg9 (*) fg) = (T . fg9) (*) (T . fg) )
assume A14: dom fg9 = cod fg ; ::_thesis: T . (fg9 (*) fg) = (T . fg9) (*) (T . fg)
consider f being Morphism of C, g being Morphism of D such that
A15: fg = [f,g] by DOMAIN_1:1;
 T . (f,g) = T . fg by A15;
then A16: T . fg = g by FUNCT_3:def_5;
consider f9 being Morphism of C, g9 being Morphism of D such that
A17: fg9 = [f9,g9] by DOMAIN_1:1;
 T . (f9,g9) = T . fg9 by A17;
then A18: T . fg9 = g9 by FUNCT_3:def_5;
 ( dom [f9,g9] = [(dom f9),(dom g9)] & cod [f,g] = [(cod f),(cod g)] ) by Th28;
then  ( dom f9 = cod f & dom g9 = cod g ) by A14, A15, A17, XTUPLE_0:1;
hence T . (fg9 (*) fg) = T . ((f9 (*) f),(g9 (*) g)) by A15, A17, Th29
.= (T . fg9) (*) (T . fg) by A18, A16, FUNCT_3:def_5 ;
::_thesis: verum
end;
hence  pr2 ( the carrier' of C, the carrier' of D) is Functor of [:C,D:],D by CAT_1:61; ::_thesis: verum
end;
end;

:: deftheorem  defines pr1 CAT_2:def_10_:_
 for C, D being Category holds pr1 (C,D) = pr1 ( the carrier' of C, the carrier' of D);

:: deftheorem  defines pr2 CAT_2:def_11_:_
 for C, D being Category holds pr2 (C,D) = pr2 ( the carrier' of C, the carrier' of D);

theorem :: CAT_2:42
canceled;

theorem :: CAT_2:43
canceled;

theorem :: CAT_2:44
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
let C, D be Category; ::_thesis: for c being Object of C
for d being Object of D holds (Obj (pr1 (C,D))) . (c,d) = c
let c be Object of C; ::_thesis: for d being Object of D holds (Obj (pr1 (C,D))) . (c,d) = c
let d be Object of D; ::_thesis: (Obj (pr1 (C,D))) . (c,d) = c
 ( id [c,d] = [(id c),(id d)] & (pr1 (C,D)) . ((id c),(id d)) = id c ) by Th31, FUNCT_3:def_4;
hence  (Obj (pr1 (C,D))) . (c,d) = c by CAT_1:67; ::_thesis: verum
end;

theorem :: CAT_2:45
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
let C, D be Category; ::_thesis: for c being Object of C
for d being Object of D holds (Obj (pr2 (C,D))) . (c,d) = d
let c be Object of C; ::_thesis: for d being Object of D holds (Obj (pr2 (C,D))) . (c,d) = d
let d be Object of D; ::_thesis: (Obj (pr2 (C,D))) . (c,d) = d
 ( id [c,d] = [(id c),(id d)] & (pr2 (C,D)) . ((id c),(id d)) = id d ) by Th31, FUNCT_3:def_5;
hence  (Obj (pr2 (C,D))) . (c,d) = d by CAT_1:67; ::_thesis: verum
end;

definition
let C, D, D9 be Category;
let T be Functor of C,D;
let T9 be Functor of C,D9;
:: original: <:
redefine func<:T,T9:> ->  Functor of C,[:D,D9:];
coherence
 <:T,T9:> is Functor of C,[:D,D9:]
proof
reconsider S = <:T,T9:> as Function of the carrier' of C, the carrier' of [:D,D9:] ;
now__::_thesis:_(_(_for_c_being_Object_of_C_ex_dd9_being_Object_of_[:D,D9:]_st_S_._(id_c)_=_id_dd9_)_&_(_for_f_being_Morphism_of_C_holds_
(_S_._(id_(dom_f))_=_id_(dom_(S_._f))_&_S_._(id_(cod_f))_=_id_(cod_(S_._f))_)_)_&_(_for_f,_g_being_Morphism_of_C_st_dom_g_=_cod_f_holds_
S_._(g_(*)_f)_=_(S_._g)_(*)_(S_._f)_)_)
thus  for c being Object of C ex dd9 being Object of [:D,D9:] st S . (id c) = id dd9 ::_thesis: ( ( for f being Morphism of C holds
( S . (id (dom f)) = id (dom (S . f)) & S . (id (cod f)) = id (cod (S . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds
S . (g (*) f) = (S . g) (*) (S . f) ) )
proof
let c be Object of C; ::_thesis: ex dd9 being Object of [:D,D9:] st S . (id c) = id dd9
set d = (Obj T) . c;
set d9 = (Obj T9) . c;
take dd9 = [((Obj T) . c),((Obj T9) . c)]; ::_thesis: S . (id c) = id dd9
thus S . (id c) = [(T . (id c)),(T9 . (id c))] by FUNCT_3:59
.= [(id ((Obj T) . c)),(T9 . (id c))] by CAT_1:68
.= [(id ((Obj T) . c)),(id ((Obj T9) . c))] by CAT_1:68
.= id dd9 by Th31 ; ::_thesis: verum
end;
thus  for f being Morphism of C holds
( S . (id (dom f)) = id (dom (S . f)) & S . (id (cod f)) = id (cod (S . f)) ) ::_thesis: for f, g being Morphism of C st dom g = cod f holds
S . (g (*) f) = (S . g) (*) (S . f)
proof
let f be Morphism of C; ::_thesis: ( S . (id (dom f)) = id (dom (S . f)) & S . (id (cod f)) = id (cod (S . f)) )
 ( T . (id (dom f)) = id (dom (T . f)) & T9 . (id (dom f)) = id (dom (T9 . f)) ) by CAT_1:63;
hence S . (id (dom f)) = [(id (dom (T . f))),(id (dom (T9 . f)))] by FUNCT_3:59
.= id [(dom (T . f)),(dom (T9 . f))] by Th31
.= id (dom [(T . f),(T9 . f)]) by Th28
.= id (dom (S . f)) by FUNCT_3:59 ;
::_thesis: S . (id (cod f)) = id (cod (S . f))
 ( T . (id (cod f)) = id (cod (T . f)) & T9 . (id (cod f)) = id (cod (T9 . f)) ) by CAT_1:63;
hence S . (id (cod f)) = [(id (cod (T . f))),(id (cod (T9 . f)))] by FUNCT_3:59
.= id [(cod (T . f)),(cod (T9 . f))] by Th31
.= id (cod [(T . f),(T9 . f)]) by Th28
.= id (cod (S . f)) by FUNCT_3:59 ;
::_thesis: verum
end;
let f, g be Morphism of C; ::_thesis: ( dom g = cod f implies S . (g (*) f) = (S . g) (*) (S . f) )
assume A1: dom g = cod f ; ::_thesis: S . (g (*) f) = (S . g) (*) (S . f)
then A2: ( dom (T . g) = cod (T . f) & dom (T9 . g) = cod (T9 . f) ) by CAT_1:64;
 ( T . (g (*) f) = (T . g) (*) (T . f) & T9 . (g (*) f) = (T9 . g) (*) (T9 . f) ) by A1, CAT_1:64;
hence S . (g (*) f) = [((T . g) (*) (T . f)),((T9 . g) (*) (T9 . f))] by FUNCT_3:59
.= [(T . g),(T9 . g)] (*) [(T . f),(T9 . f)] by A2, Th29
.= (S . g) (*) [(T . f),(T9 . f)] by FUNCT_3:59
.= (S . g) (*) (S . f) by FUNCT_3:59 ;
::_thesis: verum
end;
hence  <:T,T9:> is Functor of C,[:D,D9:] by CAT_1:61; ::_thesis: verum
end;
end;

theorem :: CAT_2:46
canceled;

theorem :: CAT_2:47
for C, D, D9 being Category
for T being Functor of C,D
for T9 being Functor of C,D9
for c being Object of C holds (Obj <:T,T9:>) . c = [((Obj T) . c),((Obj T9) . c)]
proof
let C, D, D9 be Category; ::_thesis: for T being Functor of C,D
for T9 being Functor of C,D9
for c being Object of C holds (Obj <:T,T9:>) . c = [((Obj T) . c),((Obj T9) . c)]
let T be Functor of C,D; ::_thesis: for T9 being Functor of C,D9
for c being Object of C holds (Obj <:T,T9:>) . c = [((Obj T) . c),((Obj T9) . c)]
let T9 be Functor of C,D9; ::_thesis: for c being Object of C holds (Obj <:T,T9:>) . c = [((Obj T) . c),((Obj T9) . c)]
let c be Object of C; ::_thesis: (Obj <:T,T9:>) . c = [((Obj T) . c),((Obj T9) . c)]
A1: ( T . (id c) = id ((Obj T) . c) & T9 . (id c) = id ((Obj T9) . c) ) by CAT_1:68;
 ( <:T,T9:> . (id c) = [(T . (id c)),(T9 . (id c))] & [(id ((Obj T) . c)),(id ((Obj T9) . c))] = id [((Obj T) . c),((Obj T9) . c)] ) by Th31, FUNCT_3:59;
hence  (Obj <:T,T9:>) . c = [((Obj T) . c),((Obj T9) . c)] by A1, CAT_1:67; ::_thesis: verum
end;

theorem Th48: :: CAT_2:48
for C, D, C9, D9 being Category
for T being Functor of C,D
for T9 being Functor of C9,D9 holds [:T,T9:] = <:(T * (pr1 (C,C9))),(T9 * (pr2 (C,C9))):>
proof
let C, D, C9, D9 be Category; ::_thesis: for T being Functor of C,D
for T9 being Functor of C9,D9 holds [:T,T9:] = <:(T * (pr1 (C,C9))),(T9 * (pr2 (C,C9))):>
let T be Functor of C,D; ::_thesis: for T9 being Functor of C9,D9 holds [:T,T9:] = <:(T * (pr1 (C,C9))),(T9 * (pr2 (C,C9))):>
let T9 be Functor of C9,D9; ::_thesis: [:T,T9:] = <:(T * (pr1 (C,C9))),(T9 * (pr2 (C,C9))):>
 ( dom T = the carrier' of C & dom T9 = the carrier' of C9 ) by FUNCT_2:def_1;
hence  [:T,T9:] = <:(T * (pr1 (C,C9))),(T9 * (pr2 (C,C9))):> by FUNCT_3:66; ::_thesis: verum
end;

definition
let C, C9, D, D9 be Category;
let T be Functor of C,D;
let T9 be Functor of C9,D9;
:: original: [:
redefine func[:T,T9:] ->  Functor of [:C,C9:],[:D,D9:];
coherence
 [:T,T9:] is Functor of [:C,C9:],[:D,D9:]
proof
 [:T,T9:] = <:(T * (pr1 (C,C9))),(T9 * (pr2 (C,C9))):> by Th48;
hence  [:T,T9:] is Functor of [:C,C9:],[:D,D9:] ; ::_thesis: verum
end;
end;

theorem :: CAT_2:49
canceled;

theorem :: CAT_2:50
for C, D, C9, D9 being Category
for T being Functor of C,D
for T9 being Functor of C9,D9
for c being Object of C
for c9 being Object of C9 holds (Obj [:T,T9:]) . (c,c9) = [((Obj T) . c),((Obj T9) . c9)]
proof
let C, D, C9, D9 be Category; ::_thesis: for T being Functor of C,D
for T9 being Functor of C9,D9
for c being Object of C
for c9 being Object of C9 holds (Obj [:T,T9:]) . (c,c9) = [((Obj T) . c),((Obj T9) . c9)]
let T be Functor of C,D; ::_thesis: for T9 being Functor of C9,D9
for c being Object of C
for c9 being Object of C9 holds (Obj [:T,T9:]) . (c,c9) = [((Obj T) . c),((Obj T9) . c9)]
let T9 be Functor of C9,D9; ::_thesis: for c being Object of C
for c9 being Object of C9 holds (Obj [:T,T9:]) . (c,c9) = [((Obj T) . c),((Obj T9) . c9)]
let c be Object of C; ::_thesis: for c9 being Object of C9 holds (Obj [:T,T9:]) . (c,c9) = [((Obj T) . c),((Obj T9) . c9)]
let c9 be Object of C9; ::_thesis: (Obj [:T,T9:]) . (c,c9) = [((Obj T) . c),((Obj T9) . c9)]
A1: ( T . (id c) = id ((Obj T) . c) & T9 . (id c9) = id ((Obj T9) . c9) ) by CAT_1:68;
A2: [(id ((Obj T) . c)),(id ((Obj T9) . c9))] = id [((Obj T) . c),((Obj T9) . c9)] by Th31;
 ( [:T,T9:] . ((id c),(id c9)) = [(T . (id c)),(T9 . (id c9))] & [(id c),(id c9)] = id [c,c9] ) by Th31, FUNCT_3:75;
hence  (Obj [:T,T9:]) . (c,c9) = [((Obj T) . c),((Obj T9) . c9)] by A1, A2, CAT_1:67; ::_thesis: verum
end;