:: COMMACAT semantic presentation

begin

deffunc H1( CatStr ) ->  set = the carrier of $1;

deffunc H2( CatStr ) ->  set = the carrier' of $1;


definition
let C, D, E be Category;
let F be Functor of C,E;
let G be Functor of D,E;
given c1 being Object of C, d1 being Object of D, f1 being Morphism of E such that A1: f1 in Hom ((F . c1),(G . d1)) ;
func commaObjs (F,G) ->  non empty Subset of [:[: the carrier of C, the carrier of D:], the carrier' of E:] equals :Def1: :: COMMACAT:def 1
 {  [[c,d],f] where c is Object of C, d is Object of D, f is Morphism of E : f in Hom ((F . c),(G . d))  }  ;
coherence
  {  [[c,d],f] where c is Object of C, d is Object of D, f is Morphism of E : f in Hom ((F . c),(G . d))  }  is non empty Subset of [:[: the carrier of C, the carrier of D:], the carrier' of E:]
proof
A2:  {  [[c,d],f] where c is Object of C, d is Object of D, f is Morphism of E : f in Hom ((F . c),(G . d))  }  c= [:[: the carrier of C, the carrier of D:], the carrier' of E:]
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  [[c,d],f] where c is Object of C, d is Object of D, f is Morphism of E : f in Hom ((F . c),(G . d))  }  or x in [:[: the carrier of C, the carrier of D:], the carrier' of E:] )
assume  x in  {  [[c,d],f] where c is Object of C, d is Object of D, f is Morphism of E : f in Hom ((F . c),(G . d))  }  ; ::_thesis: x in [:[: the carrier of C, the carrier of D:], the carrier' of E:]
then  ex c being Object of C ex d being Object of D ex f being Morphism of E st
( x = [[c,d],f] & f in Hom ((F . c),(G . d)) ) ;
hence  x in [:[: the carrier of C, the carrier of D:], the carrier' of E:] ; ::_thesis: verum
end;
 [[c1,d1],f1] in  {  [[c,d],f] where c is Object of C, d is Object of D, f is Morphism of E : f in Hom ((F . c),(G . d))  }  by A1;
hence   {  [[c,d],f] where c is Object of C, d is Object of D, f is Morphism of E : f in Hom ((F . c),(G . d))  }  is non empty Subset of [:[: the carrier of C, the carrier of D:], the carrier' of E:] by A2; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines commaObjs COMMACAT:def_1_:_
 for C, D, E being Category
for F being Functor of C,E
for G being Functor of D,E st ex c1 being Object of C ex d1 being Object of D ex f1 being Morphism of E st f1 in Hom ((F . c1),(G . d1)) holds
commaObjs (F,G) =  {  [[c,d],f] where c is Object of C, d is Object of D, f is Morphism of E : f in Hom ((F . c),(G . d))  }  ;


theorem Th1: :: COMMACAT:1
for C, D, E being Category
for F being Functor of C,E
for G being Functor of D,E
for o being Element of commaObjs (F,G) st ex c being Object of C ex d being Object of D ex f being Morphism of E st f in Hom ((F . c),(G . d)) holds
( o = [[(o `11),(o `12)],(o `2)] & o `2 in Hom ((F . (o `11)),(G . (o `12))) & dom (o `2) = F . (o `11) & cod (o `2) = G . (o `12) )
proof
let C, D, E be Category; ::_thesis: for F being Functor of C,E
for G being Functor of D,E
for o being Element of commaObjs (F,G) st ex c being Object of C ex d being Object of D ex f being Morphism of E st f in Hom ((F . c),(G . d)) holds
( o = [[(o `11),(o `12)],(o `2)] & o `2 in Hom ((F . (o `11)),(G . (o `12))) & dom (o `2) = F . (o `11) & cod (o `2) = G . (o `12) )
let F be Functor of C,E; ::_thesis: for G being Functor of D,E
for o being Element of commaObjs (F,G) st ex c being Object of C ex d being Object of D ex f being Morphism of E st f in Hom ((F . c),(G . d)) holds
( o = [[(o `11),(o `12)],(o `2)] & o `2 in Hom ((F . (o `11)),(G . (o `12))) & dom (o `2) = F . (o `11) & cod (o `2) = G . (o `12) )
let G be Functor of D,E; ::_thesis: for o being Element of commaObjs (F,G) st ex c being Object of C ex d being Object of D ex f being Morphism of E st f in Hom ((F . c),(G . d)) holds
( o = [[(o `11),(o `12)],(o `2)] & o `2 in Hom ((F . (o `11)),(G . (o `12))) & dom (o `2) = F . (o `11) & cod (o `2) = G . (o `12) )
let o be Element of commaObjs (F,G); ::_thesis: ( ex c being Object of C ex d being Object of D ex f being Morphism of E st f in Hom ((F . c),(G . d)) implies ( o = [[(o `11),(o `12)],(o `2)] & o `2 in Hom ((F . (o `11)),(G . (o `12))) & dom (o `2) = F . (o `11) & cod (o `2) = G . (o `12) ) )
assume  ex c being Object of C ex d being Object of D ex f being Morphism of E st f in Hom ((F . c),(G . d)) ; ::_thesis: ( o = [[(o `11),(o `12)],(o `2)] & o `2 in Hom ((F . (o `11)),(G . (o `12))) & dom (o `2) = F . (o `11) & cod (o `2) = G . (o `12) )
then A1: commaObjs (F,G) =  {  [[c,d],f] where c is Object of C, d is Object of D, f is Morphism of E : f in Hom ((F . c),(G . d))  }  by Def1;
 o in commaObjs (F,G) ;
then consider c being Object of C, d being Object of D, f being Morphism of E such that
A2: o = [[c,d],f] and
A3: f in Hom ((F . c),(G . d)) by A1;
A4: o `2 = f by A2, MCART_1:7;
 ( o `11 = c & o `12 = d ) by A2, MCART_1:85;
hence  ( o = [[(o `11),(o `12)],(o `2)] & o `2 in Hom ((F . (o `11)),(G . (o `12))) & dom (o `2) = F . (o `11) & cod (o `2) = G . (o `12) ) by A2, A3, A4, CAT_1:1; ::_thesis: verum
end;

definition
let C, D, E be Category;
let F be Functor of C,E;
let G be Functor of D,E;
given c1 being Object of C, d1 being Object of D, f1 being Morphism of E such that A1: f1 in Hom ((F . c1),(G . d1)) ;
func commaMorphs (F,G) ->  non empty Subset of [:[:(commaObjs (F,G)),(commaObjs (F,G)):],[: the carrier' of C, the carrier' of D:]:] equals :Def2: :: COMMACAT:def 2
 {  [[o1,o2],[g,h]] where g is Morphism of C, h is Morphism of D, o1, o2 is Element of commaObjs (F,G) : ( dom g = o1 `11 & cod g = o2 `11 & dom h = o1 `12 & cod h = o2 `12 & (o2 `2) (*) (F . g) = (G . h) (*) (o1 `2) )  }  ;
coherence
  {  [[o1,o2],[g,h]] where g is Morphism of C, h is Morphism of D, o1, o2 is Element of commaObjs (F,G) : ( dom g = o1 `11 & cod g = o2 `11 & dom h = o1 `12 & cod h = o2 `12 & (o2 `2) (*) (F . g) = (G . h) (*) (o1 `2) )  }  is non empty Subset of [:[:(commaObjs (F,G)),(commaObjs (F,G)):],[: the carrier' of C, the carrier' of D:]:]
proof
 commaObjs (F,G) =  {  [[c,d],f] where c is Object of C, d is Object of D, f is Morphism of E : f in Hom ((F . c),(G . d))  }  by A1, Def1;
then  [[c1,d1],f1] in commaObjs (F,G) by A1;
then reconsider o = [[c1,d1],f1] as Element of commaObjs (F,G) ;
set X =  {  [[o1,o2],[g,h]] where g is Morphism of C, h is Morphism of D, o1, o2 is Element of commaObjs (F,G) : ( dom g = o1 `11 & cod g = o2 `11 & dom h = o1 `12 & cod h = o2 `12 & (o2 `2) (*) (F . g) = (G . h) (*) (o1 `2) )  }  ;
A2: ( dom (id d1) = d1 & cod (id d1) = d1 ) ;
A3: ( (o `1) `1 = o `11 & (o `1) `2 = o `12 ) by MCART_1:def_14, MCART_1:def_15;
A4:  {  [[o1,o2],[g,h]] where g is Morphism of C, h is Morphism of D, o1, o2 is Element of commaObjs (F,G) : ( dom g = o1 `11 & cod g = o2 `11 & dom h = o1 `12 & cod h = o2 `12 & (o2 `2) (*) (F . g) = (G . h) (*) (o1 `2) )  }  c= [:[:(commaObjs (F,G)),(commaObjs (F,G)):],[: the carrier' of C, the carrier' of D:]:]
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  [[o1,o2],[g,h]] where g is Morphism of C, h is Morphism of D, o1, o2 is Element of commaObjs (F,G) : ( dom g = o1 `11 & cod g = o2 `11 & dom h = o1 `12 & cod h = o2 `12 & (o2 `2) (*) (F . g) = (G . h) (*) (o1 `2) )  }  or x in [:[:(commaObjs (F,G)),(commaObjs (F,G)):],[: the carrier' of C, the carrier' of D:]:] )
assume  x in  {  [[o1,o2],[g,h]] where g is Morphism of C, h is Morphism of D, o1, o2 is Element of commaObjs (F,G) : ( dom g = o1 `11 & cod g = o2 `11 & dom h = o1 `12 & cod h = o2 `12 & (o2 `2) (*) (F . g) = (G . h) (*) (o1 `2) )  }  ; ::_thesis: x in [:[:(commaObjs (F,G)),(commaObjs (F,G)):],[: the carrier' of C, the carrier' of D:]:]
then  ex g being Morphism of C ex h being Morphism of D ex o1, o2 being Element of commaObjs (F,G) st
( x = [[o1,o2],[g,h]] & dom g = o1 `11 & cod g = o2 `11 & dom h = o1 `12 & cod h = o2 `12 & (o2 `2) (*) (F . g) = (G . h) (*) (o1 `2) ) ;
hence  x in [:[:(commaObjs (F,G)),(commaObjs (F,G)):],[: the carrier' of C, the carrier' of D:]:] ; ::_thesis: verum
end;
A5: ( [c1,d1] `2 = d1 & o `2 = f1 ) by MCART_1:7;
A6: ( o `1 = [c1,d1] & [c1,d1] `1 = c1 ) by MCART_1:7;
 cod f1 = G . d1 by A1, CAT_1:1;
then A7: (id (G . d1)) (*) f1 = f1 by CAT_1:21;
 dom f1 = F . c1 by A1, CAT_1:1;
then A8: f1 (*) (id (F . c1)) = f1 by CAT_1:22;
A9: ( F . (id c1) = id (F . c1) & G . (id d1) = id (G . d1) ) by CAT_1:71;
 ( dom (id c1) = c1 & cod (id c1) = c1 ) ;
then  [[o,o],[(id c1),(id d1)]] in  {  [[o1,o2],[g,h]] where g is Morphism of C, h is Morphism of D, o1, o2 is Element of commaObjs (F,G) : ( dom g = o1 `11 & cod g = o2 `11 & dom h = o1 `12 & cod h = o2 `12 & (o2 `2) (*) (F . g) = (G . h) (*) (o1 `2) )  }  by A2, A3, A6, A5, A8, A7, A9;
hence   {  [[o1,o2],[g,h]] where g is Morphism of C, h is Morphism of D, o1, o2 is Element of commaObjs (F,G) : ( dom g = o1 `11 & cod g = o2 `11 & dom h = o1 `12 & cod h = o2 `12 & (o2 `2) (*) (F . g) = (G . h) (*) (o1 `2) )  }  is non empty Subset of [:[:(commaObjs (F,G)),(commaObjs (F,G)):],[: the carrier' of C, the carrier' of D:]:] by A4; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines commaMorphs COMMACAT:def_2_:_
 for C, D, E being Category
for F being Functor of C,E
for G being Functor of D,E st ex c1 being Object of C ex d1 being Object of D ex f1 being Morphism of E st f1 in Hom ((F . c1),(G . d1)) holds
commaMorphs (F,G) =  {  [[o1,o2],[g,h]] where g is Morphism of C, h is Morphism of D, o1, o2 is Element of commaObjs (F,G) : ( dom g = o1 `11 & cod g = o2 `11 & dom h = o1 `12 & cod h = o2 `12 & (o2 `2) (*) (F . g) = (G . h) (*) (o1 `2) )  }  ;


definition
let C, D, E be Category;
let F be Functor of C,E;
let G be Functor of D,E;
let k be Element of commaMorphs (F,G);
:: original: `11
redefine funck `11  ->  Element of commaObjs (F,G);
coherence
 k `11 is Element of commaObjs (F,G)
proof
thus  k `11 is Element of commaObjs (F,G) ; ::_thesis: verum
end;
:: original: `12
redefine funck `12  ->  Element of commaObjs (F,G);
coherence
 k `12 is Element of commaObjs (F,G)
proof
thus  k `12 is Element of commaObjs (F,G) ; ::_thesis: verum
end;
end;

theorem Th2: :: COMMACAT:2
for C, D, E being Category
for F being Functor of C,E
for G being Functor of D,E
for k being Element of commaMorphs (F,G) st ex c being Object of C ex d being Object of D ex f being Morphism of E st f in Hom ((F . c),(G . d)) holds
( k = [[(k `11),(k `12)],[(k `21),(k `22)]] & dom (k `21) = (k `11) `11 & cod (k `21) = (k `12) `11 & dom (k `22) = (k `11) `12 & cod (k `22) = (k `12) `12 & ((k `12) `2) (*) (F . (k `21)) = (G . (k `22)) (*) ((k `11) `2) )
proof
let C, D, E be Category; ::_thesis: for F being Functor of C,E
for G being Functor of D,E
for k being Element of commaMorphs (F,G) st ex c being Object of C ex d being Object of D ex f being Morphism of E st f in Hom ((F . c),(G . d)) holds
( k = [[(k `11),(k `12)],[(k `21),(k `22)]] & dom (k `21) = (k `11) `11 & cod (k `21) = (k `12) `11 & dom (k `22) = (k `11) `12 & cod (k `22) = (k `12) `12 & ((k `12) `2) (*) (F . (k `21)) = (G . (k `22)) (*) ((k `11) `2) )
let F be Functor of C,E; ::_thesis: for G being Functor of D,E
for k being Element of commaMorphs (F,G) st ex c being Object of C ex d being Object of D ex f being Morphism of E st f in Hom ((F . c),(G . d)) holds
( k = [[(k `11),(k `12)],[(k `21),(k `22)]] & dom (k `21) = (k `11) `11 & cod (k `21) = (k `12) `11 & dom (k `22) = (k `11) `12 & cod (k `22) = (k `12) `12 & ((k `12) `2) (*) (F . (k `21)) = (G . (k `22)) (*) ((k `11) `2) )
let G be Functor of D,E; ::_thesis: for k being Element of commaMorphs (F,G) st ex c being Object of C ex d being Object of D ex f being Morphism of E st f in Hom ((F . c),(G . d)) holds
( k = [[(k `11),(k `12)],[(k `21),(k `22)]] & dom (k `21) = (k `11) `11 & cod (k `21) = (k `12) `11 & dom (k `22) = (k `11) `12 & cod (k `22) = (k `12) `12 & ((k `12) `2) (*) (F . (k `21)) = (G . (k `22)) (*) ((k `11) `2) )
let k be Element of commaMorphs (F,G); ::_thesis: ( ex c being Object of C ex d being Object of D ex f being Morphism of E st f in Hom ((F . c),(G . d)) implies ( k = [[(k `11),(k `12)],[(k `21),(k `22)]] & dom (k `21) = (k `11) `11 & cod (k `21) = (k `12) `11 & dom (k `22) = (k `11) `12 & cod (k `22) = (k `12) `12 & ((k `12) `2) (*) (F . (k `21)) = (G . (k `22)) (*) ((k `11) `2) ) )
assume  ex c being Object of C ex d being Object of D ex f being Morphism of E st f in Hom ((F . c),(G . d)) ; ::_thesis: ( k = [[(k `11),(k `12)],[(k `21),(k `22)]] & dom (k `21) = (k `11) `11 & cod (k `21) = (k `12) `11 & dom (k `22) = (k `11) `12 & cod (k `22) = (k `12) `12 & ((k `12) `2) (*) (F . (k `21)) = (G . (k `22)) (*) ((k `11) `2) )
then A1: commaMorphs (F,G) =  {  [[o1,o2],[g,h]] where g is Morphism of C, h is Morphism of D, o1, o2 is Element of commaObjs (F,G) : ( dom g = o1 `11 & cod g = o2 `11 & dom h = o1 `12 & cod h = o2 `12 & (o2 `2) (*) (F . g) = (G . h) (*) (o1 `2) )  }  by Def2;
 k in commaMorphs (F,G) ;
then consider g being Morphism of C, h being Morphism of D, o1, o2 being Element of commaObjs (F,G) such that
A2: k = [[o1,o2],[g,h]] and
A3: ( dom g = o1 `11 & cod g = o2 `11 & dom h = o1 `12 & cod h = o2 `12 & (o2 `2) (*) (F . g) = (G . h) (*) (o1 `2) ) by A1;
A4: k `21 = g by A2, MCART_1:85;
 ( k `11 = o1 & k `12 = o2 ) by A2, MCART_1:85;
hence  ( k = [[(k `11),(k `12)],[(k `21),(k `22)]] & dom (k `21) = (k `11) `11 & cod (k `21) = (k `12) `11 & dom (k `22) = (k `11) `12 & cod (k `22) = (k `12) `12 & ((k `12) `2) (*) (F . (k `21)) = (G . (k `22)) (*) ((k `11) `2) ) by A2, A3, A4, MCART_1:85; ::_thesis: verum
end;

definition
let C, D, E be Category;
let F be Functor of C,E;
let G be Functor of D,E;
let k1, k2 be Element of commaMorphs (F,G);
given c1 being Object of C, d1 being Object of D, f1 being Morphism of E such that A1: f1 in Hom ((F . c1),(G . d1)) ;
assume A2: k1 `12 = k2 `11 ;
funck2 * k1 ->  Element of commaMorphs (F,G) equals :Def3: :: COMMACAT:def 3
[[(k1 `11),(k2 `12)],[((k2 `21) (*) (k1 `21)),((k2 `22) (*) (k1 `22))]];
coherence
 [[(k1 `11),(k2 `12)],[((k2 `21) (*) (k1 `21)),((k2 `22) (*) (k1 `22))]] is Element of commaMorphs (F,G)
proof
set k22 = (k2 `22) (*) (k1 `22);
set k21 = (k2 `21) (*) (k1 `21);
A3: ( F . (cod (k2 `21)) = cod (F . (k2 `21)) & dom (F . (k2 `21)) = F . (dom (k2 `21)) ) by CAT_1:72;
A4: cod (F . (k1 `21)) = F . (cod (k1 `21)) by CAT_1:72;
A5: cod ((k1 `12) `2) = G . ((k1 `12) `12) by A1, Th1;
A6: dom (k1 `22) = (k1 `11) `12 by A1, Th2;
A7: ( ((k2 `12) `2) (*) (F . (k2 `21)) = (G . (k2 `22)) (*) ((k2 `11) `2) & dom ((k2 `12) `2) = F . ((k2 `12) `11) ) by A1, Th1, Th2;
A8: cod (G . (k1 `22)) = G . (cod (k1 `22)) by CAT_1:72;
A9: ( ((k1 `12) `2) (*) (F . (k1 `21)) = (G . (k1 `22)) (*) ((k1 `11) `2) & dom ((k1 `12) `2) = F . ((k1 `12) `11) ) by A1, Th1, Th2;
A10: dom (G . (k2 `22)) = G . (dom (k2 `22)) by CAT_1:72;
A11: ( cod ((k1 `11) `2) = G . ((k1 `11) `12) & dom (G . (k1 `22)) = G . (dom (k1 `22)) ) by A1, Th1, CAT_1:72;
A12: cod (k2 `21) = (k2 `12) `11 by A1, Th2;
A13: commaMorphs (F,G) =  {  [[o1,o2],[g,h]] where g is Morphism of C, h is Morphism of D, o1, o2 is Element of commaObjs (F,G) : ( dom g = o1 `11 & cod g = o2 `11 & dom h = o1 `12 & cod h = o2 `12 & (o2 `2) (*) (F . g) = (G . h) (*) (o1 `2) )  }  by A1, Def2;
A14: dom (k2 `22) = (k2 `11) `12 by A1, Th2;
A15: cod (k1 `22) = (k1 `12) `12 by A1, Th2;
then A16: ( dom ((k2 `22) (*) (k1 `22)) = dom (k1 `22) & cod ((k2 `22) (*) (k1 `22)) = cod (k2 `22) ) by A2, A14, CAT_1:17;
A17: ( dom (k1 `21) = (k1 `11) `11 & cod (k2 `22) = (k2 `12) `12 ) by A1, Th2;
A18: cod (k1 `21) = (k1 `12) `11 by A1, Th2;
A19: dom (k2 `21) = (k2 `11) `11 by A1, Th2;
then A20: ( dom ((k2 `21) (*) (k1 `21)) = dom (k1 `21) & cod ((k2 `21) (*) (k1 `21)) = cod (k2 `21) ) by A2, A18, CAT_1:17;
((k2 `12) `2) (*) (F . ((k2 `21) (*) (k1 `21))) = ((k2 `12) `2) (*) ((F . (k2 `21)) (*) (F . (k1 `21))) by A2, A18, A19, CAT_1:64
.= ((G . (k2 `22)) (*) ((k2 `11) `2)) (*) (F . (k1 `21)) by A2, A18, A19, A12, A7, A3, A4, CAT_1:18
.= (G . (k2 `22)) (*) ((G . (k1 `22)) (*) ((k1 `11) `2)) by A2, A18, A14, A9, A5, A4, A10, CAT_1:18
.= ((G . (k2 `22)) (*) (G . (k1 `22))) (*) ((k1 `11) `2) by A2, A6, A15, A14, A10, A11, A8, CAT_1:18
.= (G . ((k2 `22) (*) (k1 `22))) (*) ((k1 `11) `2) by A2, A15, A14, CAT_1:64 ;
then  [[(k1 `11),(k2 `12)],[((k2 `21) (*) (k1 `21)),((k2 `22) (*) (k1 `22))]] in commaMorphs (F,G) by A6, A12, A17, A13, A20, A16;
hence  [[(k1 `11),(k2 `12)],[((k2 `21) (*) (k1 `21)),((k2 `22) (*) (k1 `22))]] is Element of commaMorphs (F,G) ; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines * COMMACAT:def_3_:_
 for C, D, E being Category
for F being Functor of C,E
for G being Functor of D,E
for k1, k2 being Element of commaMorphs (F,G) st ex c1 being Object of C ex d1 being Object of D ex f1 being Morphism of E st f1 in Hom ((F . c1),(G . d1)) & k1 `12 = k2 `11 holds
k2 * k1 = [[(k1 `11),(k2 `12)],[((k2 `21) (*) (k1 `21)),((k2 `22) (*) (k1 `22))]];

definition
let C, D, E be Category;
let F be Functor of C,E;
let G be Functor of D,E;
func commaComp (F,G) ->  PartFunc of [:(commaMorphs (F,G)),(commaMorphs (F,G)):],(commaMorphs (F,G)) means :Def4: :: COMMACAT:def 4
( dom it =  {  [k1,k2] where k1, k2 is Element of commaMorphs (F,G) : k1 `11 = k2 `12  }  & ( for k, k9 being Element of commaMorphs (F,G) st [k,k9] in dom it holds
it . [k,k9] = k * k9 ) );
existence
 ex b1 being PartFunc of [:(commaMorphs (F,G)),(commaMorphs (F,G)):],(commaMorphs (F,G)) st
( dom b1 =  {  [k1,k2] where k1, k2 is Element of commaMorphs (F,G) : k1 `11 = k2 `12  }  & ( for k, k9 being Element of commaMorphs (F,G) st [k,k9] in dom b1 holds
b1 . [k,k9] = k * k9 ) )
proof
defpred S1[ set , set ] means  ex k1, k2 being Element of commaMorphs (F,G) st
( $1 = [k1,k2] & $2 = k1 * k2 );
set X =  {  [k1,k2] where k1, k2 is Element of commaMorphs (F,G) : k1 `11 = k2 `12  }  ;
A1: for x being set st x in  {  [k1,k2] where k1, k2 is Element of commaMorphs (F,G) : k1 `11 = k2 `12  }  holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in  {  [k1,k2] where k1, k2 is Element of commaMorphs (F,G) : k1 `11 = k2 `12  }  implies ex y being set st S1[x,y] )
assume  x in  {  [k1,k2] where k1, k2 is Element of commaMorphs (F,G) : k1 `11 = k2 `12  }  ; ::_thesis: ex y being set st S1[x,y]
then consider k1, k2 being Element of commaMorphs (F,G) such that
A2: x = [k1,k2] and
 k1 `11 = k2 `12 ;
reconsider y = k1 * k2 as set ;
take  y ; ::_thesis: S1[x,y]
take  k1 ; ::_thesis: ex k2 being Element of commaMorphs (F,G) st
( x = [k1,k2] & y = k1 * k2 )
take  k2 ; ::_thesis: ( x = [k1,k2] & y = k1 * k2 )
thus  ( x = [k1,k2] & y = k1 * k2 ) by A2; ::_thesis: verum
end;
consider f being Function such that
A3: ( dom f =  {  [k1,k2] where k1, k2 is Element of commaMorphs (F,G) : k1 `11 = k2 `12  }  & ( for x being set st x in  {  [k1,k2] where k1, k2 is Element of commaMorphs (F,G) : k1 `11 = k2 `12  }  holds
S1[x,f . x] ) ) from CLASSES1:sch_1(A1);
A4: rng f c= commaMorphs (F,G)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in commaMorphs (F,G) )
assume  x in rng f ; ::_thesis: x in commaMorphs (F,G)
then consider y being set  such that
A5: y in dom f and
A6: x = f . y by FUNCT_1:def_3;
 ex k1, k2 being Element of commaMorphs (F,G) st
( y = [k1,k2] & f . y = k1 * k2 ) by A3, A5;
hence  x in commaMorphs (F,G) by A6; ::_thesis: verum
end;
 dom f c= [:(commaMorphs (F,G)),(commaMorphs (F,G)):]
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom f or x in [:(commaMorphs (F,G)),(commaMorphs (F,G)):] )
assume  x in dom f ; ::_thesis: x in [:(commaMorphs (F,G)),(commaMorphs (F,G)):]
then  ex k1, k2 being Element of commaMorphs (F,G) st
( x = [k1,k2] & k1 `11 = k2 `12 ) by A3;
hence  x in [:(commaMorphs (F,G)),(commaMorphs (F,G)):] ; ::_thesis: verum
end;
then reconsider f = f as PartFunc of [:(commaMorphs (F,G)),(commaMorphs (F,G)):],(commaMorphs (F,G)) by A4, RELSET_1:4;
take  f ; ::_thesis: ( dom f =  {  [k1,k2] where k1, k2 is Element of commaMorphs (F,G) : k1 `11 = k2 `12  }  & ( for k, k9 being Element of commaMorphs (F,G) st [k,k9] in dom f holds
f . [k,k9] = k * k9 ) )
thus  dom f =  {  [k1,k2] where k1, k2 is Element of commaMorphs (F,G) : k1 `11 = k2 `12  }  by A3; ::_thesis: for k, k9 being Element of commaMorphs (F,G) st [k,k9] in dom f holds
f . [k,k9] = k * k9
let k1, k2 be Element of commaMorphs (F,G); ::_thesis: ( [k1,k2] in dom f implies f . [k1,k2] = k1 * k2 )
assume  [k1,k2] in dom f ; ::_thesis: f . [k1,k2] = k1 * k2
then consider k, k9 being Element of commaMorphs (F,G) such that
A7: [k1,k2] = [k,k9] and
A8: f . [k1,k2] = k * k9 by A3;
 k1 = k by A7, XTUPLE_0:1;
hence  f . [k1,k2] = k1 * k2 by A7, A8, XTUPLE_0:1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being PartFunc of [:(commaMorphs (F,G)),(commaMorphs (F,G)):],(commaMorphs (F,G)) st dom b1 =  {  [k1,k2] where k1, k2 is Element of commaMorphs (F,G) : k1 `11 = k2 `12  }  & ( for k, k9 being Element of commaMorphs (F,G) st [k,k9] in dom b1 holds
b1 . [k,k9] = k * k9 ) & dom b2 =  {  [k1,k2] where k1, k2 is Element of commaMorphs (F,G) : k1 `11 = k2 `12  }  & ( for k, k9 being Element of commaMorphs (F,G) st [k,k9] in dom b2 holds
b2 . [k,k9] = k * k9 ) holds
b1 = b2
proof
let f1, f2 be PartFunc of [:(commaMorphs (F,G)),(commaMorphs (F,G)):],(commaMorphs (F,G)); ::_thesis: ( dom f1 =  {  [k1,k2] where k1, k2 is Element of commaMorphs (F,G) : k1 `11 = k2 `12  }  & ( for k, k9 being Element of commaMorphs (F,G) st [k,k9] in dom f1 holds
f1 . [k,k9] = k * k9 ) & dom f2 =  {  [k1,k2] where k1, k2 is Element of commaMorphs (F,G) : k1 `11 = k2 `12  }  & ( for k, k9 being Element of commaMorphs (F,G) st [k,k9] in dom f2 holds
f2 . [k,k9] = k * k9 ) implies f1 = f2 )
assume that
A9: ( dom f1 =  {  [k1,k2] where k1, k2 is Element of commaMorphs (F,G) : k1 `11 = k2 `12  }  & ( for k, k9 being Element of commaMorphs (F,G) st [k,k9] in dom f1 holds
f1 . [k,k9] = k * k9 ) ) and
A10: ( dom f2 =  {  [k1,k2] where k1, k2 is Element of commaMorphs (F,G) : k1 `11 = k2 `12  }  & ( for k, k9 being Element of commaMorphs (F,G) st [k,k9] in dom f2 holds
f2 . [k,k9] = k * k9 ) ) ; ::_thesis: f1 = f2
now__::_thesis:_for_x_being_set_st_x_in__{__[k1,k2]_where_k1,_k2_is_Element_of_commaMorphs_(F,G)_:_k1_`11_=_k2_`12__}__holds_
f1_._x_=_f2_._x
let x be set ; ::_thesis: ( x in  {  [k1,k2] where k1, k2 is Element of commaMorphs (F,G) : k1 `11 = k2 `12  }  implies f1 . x = f2 . x )
assume A11: x in  {  [k1,k2] where k1, k2 is Element of commaMorphs (F,G) : k1 `11 = k2 `12  }  ; ::_thesis: f1 . x = f2 . x
then consider k1, k2 being Element of commaMorphs (F,G) such that
A12: x = [k1,k2] and
 k1 `11 = k2 `12 ;
thus f1 . x = k1 * k2 by A9, A11, A12
.= f2 . x by A10, A11, A12 ; ::_thesis: verum
end;
hence  f1 = f2 by A9, A10, FUNCT_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines commaComp COMMACAT:def_4_:_
 for C, D, E being Category
for F being Functor of C,E
for G being Functor of D,E
for b6 being PartFunc of [:(commaMorphs (F,G)),(commaMorphs (F,G)):],(commaMorphs (F,G)) holds
( b6 = commaComp (F,G) iff ( dom b6 =  {  [k1,k2] where k1, k2 is Element of commaMorphs (F,G) : k1 `11 = k2 `12  }  & ( for k, k9 being Element of commaMorphs (F,G) st [k,k9] in dom b6 holds
b6 . [k,k9] = k * k9 ) ) );

definition
let C, D, E be Category;
let F be Functor of C,E;
let G be Functor of D,E;
given c1 being Object of C, d1 being Object of D, f1 being Morphism of E such that A1: f1 in Hom ((F . c1),(G . d1)) ;
funcF comma G ->  strict Category means :: COMMACAT:def 5
( the carrier of it = commaObjs (F,G) & the carrier' of it = commaMorphs (F,G) & ( for k being Element of commaMorphs (F,G) holds the Source of it . k = k `11 ) & ( for k being Element of commaMorphs (F,G) holds the Target of it . k = k `12 ) & the Comp of it = commaComp (F,G) );
existence
 ex b1 being strict Category st
( the carrier of b1 = commaObjs (F,G) & the carrier' of b1 = commaMorphs (F,G) & ( for k being Element of commaMorphs (F,G) holds the Source of b1 . k = k `11 ) & ( for k being Element of commaMorphs (F,G) holds the Target of b1 . k = k `12 ) & the Comp of b1 = commaComp (F,G) )
proof
reconsider O = commaObjs (F,G), M = commaMorphs (F,G) as non empty set ;
defpred S1[ Element of commaObjs (F,G), set ] means $2 = [[$1,$1],[(id ($1 `11)),(id ($1 `12))]];
deffunc H3( Element of commaMorphs (F,G)) ->  Element of commaObjs (F,G) = $1 `12 ;
deffunc H4( Element of commaMorphs (F,G)) ->  Element of commaObjs (F,G) = $1 `11 ;
consider D9 being Function of (commaMorphs (F,G)),(commaObjs (F,G)) such that
A2: for k being Element of commaMorphs (F,G) holds D9 . k = H4(k) from FUNCT_2:sch_4();
set I = the Function of (commaObjs (F,G)),(commaMorphs (F,G));
reconsider I = the Function of (commaObjs (F,G)),(commaMorphs (F,G)) as Function of O,M ;
reconsider a9 = commaComp (F,G) as PartFunc of [:M,M:],M ;
consider C9 being Function of (commaMorphs (F,G)),(commaObjs (F,G)) such that
A3: for k being Element of commaMorphs (F,G) holds C9 . k = H3(k) from FUNCT_2:sch_4();
reconsider D9 = D9, C9 = C9 as Function of M,O ;
set FG = CatStr(# O,M,D9,C9,a9 #);
A4: dom the Comp of CatStr(# O,M,D9,C9,a9 #) =  {  [k1,k2] where k1, k2 is Element of commaMorphs (F,G) : k1 `11 = k2 `12  }  by Def4;
A5: for f, g being Morphism of CatStr(# O,M,D9,C9,a9 #)
for k1, k2 being Element of commaMorphs (F,G) st f = k1 & g = k2 & dom g = cod f holds
g (*) f = [[(k1 `11),(k2 `12)],[((k2 `21) (*) (k1 `21)),((k2 `22) (*) (k1 `22))]]
proof
let f, g be Morphism of CatStr(# O,M,D9,C9,a9 #); ::_thesis: for k1, k2 being Element of commaMorphs (F,G) st f = k1 & g = k2 & dom g = cod f holds
g (*) f = [[(k1 `11),(k2 `12)],[((k2 `21) (*) (k1 `21)),((k2 `22) (*) (k1 `22))]]
let k1, k2 be Element of commaMorphs (F,G); ::_thesis: ( f = k1 & g = k2 & dom g = cod f implies g (*) f = [[(k1 `11),(k2 `12)],[((k2 `21) (*) (k1 `21)),((k2 `22) (*) (k1 `22))]] )
assume that
A6: ( f = k1 & g = k2 ) and
A7: dom g = cod f ; ::_thesis: g (*) f = [[(k1 `11),(k2 `12)],[((k2 `21) (*) (k1 `21)),((k2 `22) (*) (k1 `22))]]
A8: ( dom g = k2 `11 & cod f = k1 `12 ) by A2, A3, A6;
then A9: [k2,k1] in dom a9 by A4, A7;
then A10: a9 . (k2,k1) = k2 * k1 by Def4;
 g (*) f = a9 . (g,f) by A6, A9, CAT_1:def_1;
hence  g (*) f = [[(k1 `11),(k2 `12)],[((k2 `21) (*) (k1 `21)),((k2 `22) (*) (k1 `22))]] by A1, A6, A7, A8, A10, Def3; ::_thesis: verum
end;
A11: for b being Element of CatStr(# O,M,D9,C9,a9 #) holds Hom (b,b) <> {}
proof
let b be Element of CatStr(# O,M,D9,C9,a9 #); ::_thesis: Hom (b,b) <> {}
reconsider o = b as Element of commaObjs (F,G) ;
set i = [[o,o],[(id (o `11)),(id (o `12))]];
reconsider g = id (o `11) as Morphism of C ;
reconsider h = id (o `12) as Morphism of D ;
A12: dom g = o `11 by CAT_1:58;
A13: cod g = o `11 by CAT_1:58;
A14: dom h = o `12 by CAT_1:58;
A15: cod h = o `12 by CAT_1:58;
 o in commaObjs (F,G) ;
then  o in  {  [[c,d],f] where c is Object of C, d is Object of D, f is Morphism of E : f in Hom ((F . c),(G . d))  }  by A1, Def1;
then consider c being Object of C, d being Object of D, f being Morphism of E such that
A16: o = [[c,d],f] and
A17: f in Hom ((F . c),(G . d)) ;
A18: F . g = id (F . (o `11)) by CAT_1:71;
A19: G . h = id (G . (o `12)) by CAT_1:71;
A20: [[c,d],f] `2 = f ;
A21: c = o `11 by A16, MCART_1:85;
A22: d = o `12 by A16, MCART_1:85;
A23: cod (o `2) = cod f by A20, A16
.= G . d by A17, CAT_1:1
.= G . (o `12) by A22 ;
dom (o `2) = F . c by A16, A17, CAT_1:1, A20
.= F . (o `11) by A21 ;
then A24: (o `2) (*) (F . g) = o `2 by A18, CAT_1:22
.= (G . h) (*) (o `2) by A19, A23, CAT_1:21 ;
 [[o,o],[(id (o `11)),(id (o `12))]] in  {  [[o1,o2],[gg,hh]] where gg is Morphism of C, hh is Morphism of D, o1, o2 is Element of commaObjs (F,G) : ( dom gg = o1 `11 & cod gg = o2 `11 & dom hh = o1 `12 & cod hh = o2 `12 & (o2 `2) (*) (F . gg) = (G . hh) (*) (o1 `2) )  }  by A12, A13, A14, A15, A24;
then  [[o,o],[(id (o `11)),(id (o `12))]] in commaMorphs (F,G) by Def2, A1;
then reconsider i = [[o,o],[(id (o `11)),(id (o `12))]] as Morphism of CatStr(# O,M,D9,C9,a9 #) ;
A25: cod i = C9 . i
.= [[o,o],[g,h]] `12 by A3
.= b by MCART_1:85 ;
dom i = D9 . i
.= [[o,o],[g,h]] `11 by A2
.= b by MCART_1:85 ;
then  i in Hom (b,b) by A25;
hence  Hom (b,b) <> {} ; ::_thesis: verum
end;
A26: for a being Element of CatStr(# O,M,D9,C9,a9 #) ex i being Morphism of a,a st
for b being Element of CatStr(# O,M,D9,C9,a9 #) holds
( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) )
proof
let a be Element of CatStr(# O,M,D9,C9,a9 #); ::_thesis: ex i being Morphism of a,a st
for b being Element of CatStr(# O,M,D9,C9,a9 #) holds
( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) )
reconsider o = a as Element of commaObjs (F,G) ;
set i = [[o,o],[(id (o `11)),(id (o `12))]];
reconsider g = id (o `11) as Morphism of C ;
reconsider h = id (o `12) as Morphism of D ;
A27: dom g = o `11 by CAT_1:58;
A28: cod g = o `11 by CAT_1:58;
A29: dom h = o `12 by CAT_1:58;
A30: cod h = o `12 by CAT_1:58;
 o in commaObjs (F,G) ;
then  o in  {  [[c,d],f] where c is Object of C, d is Object of D, f is Morphism of E : f in Hom ((F . c),(G . d))  }  by A1, Def1;
then consider c being Object of C, d being Object of D, f being Morphism of E such that
A31: o = [[c,d],f] and
A32: f in Hom ((F . c),(G . d)) ;
A33: F . g = id (F . (o `11)) by CAT_1:71;
A34: G . h = id (G . (o `12)) by CAT_1:71;
A35: [[c,d],f] `2 = f ;
A36: c = o `11 by A31, MCART_1:85;
A37: d = o `12 by A31, MCART_1:85;
A38: cod (o `2) = cod f by A35, A31
.= G . d by A32, CAT_1:1
.= G . (o `12) by A37 ;
dom (o `2) = F . c by A31, A32, CAT_1:1, A35
.= F . (o `11) by A36 ;
then A39: (o `2) (*) (F . g) = o `2 by A33, CAT_1:22
.= (G . h) (*) (o `2) by A34, A38, CAT_1:21 ;
 [[o,o],[(id (o `11)),(id (o `12))]] in  {  [[o1,o2],[gg,hh]] where gg is Morphism of C, hh is Morphism of D, o1, o2 is Element of commaObjs (F,G) : ( dom gg = o1 `11 & cod gg = o2 `11 & dom hh = o1 `12 & cod hh = o2 `12 & (o2 `2) (*) (F . gg) = (G . hh) (*) (o1 `2) )  }  by A27, A28, A29, A30, A39;
then  [[o,o],[(id (o `11)),(id (o `12))]] in commaMorphs (F,G) by Def2, A1;
then reconsider i = [[o,o],[(id (o `11)),(id (o `12))]] as Morphism of CatStr(# O,M,D9,C9,a9 #) ;
A40: cod i = C9 . i
.= [[o,o],[g,h]] `12 by A3
.= a by MCART_1:85 ;
dom i = D9 . i
.= [[o,o],[g,h]] `11 by A2
.= a by MCART_1:85 ;
then  i in Hom (a,a) by A40;
then reconsider i = i as Morphism of a,a by CAT_1:def_5;
take  i ; ::_thesis: for b being Element of CatStr(# O,M,D9,C9,a9 #) holds
( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) )
let b be Element of CatStr(# O,M,D9,C9,a9 #); ::_thesis: ( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) )
thus  ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) ::_thesis: ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f )
proof
assume A41: Hom (a,b) <> {} ; ::_thesis: for g being Morphism of a,b holds g (*) i = g
let g be Morphism of a,b; ::_thesis: g (*) i = g
reconsider gg = g as Element of commaMorphs (F,G) ;
reconsider ii = i as Element of commaMorphs (F,G) ;
A42: commaMorphs (F,G) =  {  [[o1,o2],[g1,h1]] where g1 is Morphism of C, h1 is Morphism of D, o1, o2 is Element of commaObjs (F,G) : ( dom g1 = o1 `11 & cod g1 = o2 `11 & dom h1 = o1 `12 & cod h1 = o2 `12 & (o2 `2) (*) (F . g1) = (G . h1) (*) (o1 `2) )  }  by A1, Def2;
 gg in commaMorphs (F,G) ;
then consider g1 being Morphism of C, h1 being Morphism of D, o1, o2 being Element of commaObjs (F,G) such that
A43: gg = [[o1,o2],[g1,h1]] and
A44: dom g1 = o1 `11 and
 cod g1 = o2 `11 and
A45: dom h1 = o1 `12 and
 ( cod h1 = o2 `12 & (o2 `2) (*) (F . g1) = (G . h1) (*) (o1 `2) ) by A42;
A46: dom (commaComp (F,G)) =  {  [k1,k2] where k1, k2 is Element of commaMorphs (F,G) : k1 `11 = k2 `12  }  by Def4;
A47: ii `21 = [[o,o],[(id (o `11)),(id (o `12))]] `21
.= id (o `11) by MCART_1:85 ;
A48: ii `22 = [[o,o],[(id (o `11)),(id (o `12))]] `22
.= id (o `12) by MCART_1:85 ;
A49: o1 = [[o1,o2],[g1,h1]] `11 by MCART_1:85
.= gg `11 by A43 ;
A50: o2 = [[o1,o2],[g1,h1]] `12 by MCART_1:85
.= gg `12 by A43 ;
A51: g1 = [[o1,o2],[g1,h1]] `21 by MCART_1:85
.= gg `21 by A43 ;
A52: h1 = [[o1,o2],[g1,h1]] `22 by MCART_1:85
.= gg `22 by A43 ;
A53: dom g = a by A41, CAT_1:5;
A54: dom g = gg `11 by A2
.= [[o1,o2],[g1,h1]] `11 by A43
.= o1 by MCART_1:85 ;
A55: o1 = a by A41, CAT_1:5, A54
.= [[c,d],f] by A31 ;
A56: dom (gg `21) = dom ([[o1,o2],[g1,h1]] `21) by A43
.= dom g1 by MCART_1:85
.= o1 `11 by A44
.= [[c,d],f] `11 by A55
.= o `11 by A31 ;
A57: dom (gg `22) = dom ([[o1,o2],[g1,h1]] `22) by A43
.= dom h1 by MCART_1:85
.= o1 `12 by A45
.= [[c,d],f] `12 by A55
.= o `12 by A31 ;
A58: ii `11 = [[o,o],[(id (o `11)),(id (o `12))]] `11
.= dom g by A53, MCART_1:85
.= D9 . gg
.= gg `11 by A2 ;
A59: ii `11 = o by MCART_1:85
.= ii `12 by MCART_1:85 ;
then  gg `11 = ii `12 by A58;
then A60: [gg,ii] in dom (commaComp (F,G)) by A46;
hence g (*) i = (commaComp (F,G)) . (g,i) by CAT_1:def_1
.= gg * ii by A60, Def4
.= [[(gg `11),(gg `12)],[((gg `21) (*) (id (o `11))),((gg `22) (*) (ii `22))]] by A1, A59, Def3, A58, A47
.= [[(gg `11),(gg `12)],[(gg `21),((gg `22) (*) (ii `22))]] by A56, CAT_1:22
.= [[(gg `11),(gg `12)],[(gg `21),(gg `22)]] by CAT_1:22, A48, A57
.= g by A49, A50, A51, A52, A43 ;
::_thesis: verum
end;
thus  ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) ::_thesis: verum
proof
assume A61: Hom (b,a) <> {} ; ::_thesis: for f being Morphism of b,a holds i (*) f = f
let g be Morphism of b,a; ::_thesis: i (*) g = g
reconsider gg = g as Element of commaMorphs (F,G) ;
reconsider ii = i as Element of commaMorphs (F,G) ;
A62: commaMorphs (F,G) =  {  [[o1,o2],[g1,h1]] where g1 is Morphism of C, h1 is Morphism of D, o1, o2 is Element of commaObjs (F,G) : ( dom g1 = o1 `11 & cod g1 = o2 `11 & dom h1 = o1 `12 & cod h1 = o2 `12 & (o2 `2) (*) (F . g1) = (G . h1) (*) (o1 `2) )  }  by A1, Def2;
 gg in commaMorphs (F,G) ;
then consider g1 being Morphism of C, h1 being Morphism of D, o1, o2 being Element of commaObjs (F,G) such that
A63: gg = [[o1,o2],[g1,h1]] and
 dom g1 = o1 `11 and
A64: cod g1 = o2 `11 and
 dom h1 = o1 `12 and
A65: cod h1 = o2 `12 and
 (o2 `2) (*) (F . g1) = (G . h1) (*) (o1 `2) by A62;
A66: dom (commaComp (F,G)) =  {  [k1,k2] where k1, k2 is Element of commaMorphs (F,G) : k1 `11 = k2 `12  }  by Def4;
A67: ii `21 = [[o,o],[(id (o `11)),(id (o `12))]] `21
.= id (o `11) by MCART_1:85 ;
A68: ii `22 = [[o,o],[(id (o `11)),(id (o `12))]] `22
.= id (o `12) by MCART_1:85 ;
A69: o1 = [[o1,o2],[g1,h1]] `11 by MCART_1:85
.= gg `11 by A63 ;
A70: o2 = [[o1,o2],[g1,h1]] `12 by MCART_1:85
.= gg `12 by A63 ;
A71: g1 = [[o1,o2],[g1,h1]] `21 by MCART_1:85
.= gg `21 by A63 ;
A72: h1 = [[o1,o2],[g1,h1]] `22 by MCART_1:85
.= gg `22 by A63 ;
A73: cod g = a by A61, CAT_1:5;
A74: cod g = gg `12 by A3
.= [[o1,o2],[g1,h1]] `12 by A63
.= o2 by MCART_1:85 ;
A75: o2 = a by A61, CAT_1:5, A74
.= [[c,d],f] by A31 ;
A76: cod (gg `21) = cod ([[o1,o2],[g1,h1]] `21) by A63
.= cod g1 by MCART_1:85
.= o2 `11 by A64
.= [[c,d],f] `11 by A75
.= o `11 by A31 ;
A77: cod (gg `22) = cod ([[o1,o2],[g1,h1]] `22) by A63
.= cod h1 by MCART_1:85
.= o2 `12 by A65
.= [[c,d],f] `12 by A75
.= o `12 by A31 ;
A78: ii `11 = [[o,o],[(id (o `11)),(id (o `12))]] `11
.= cod g by A73, MCART_1:85
.= C9 . gg
.= gg `12 by A3 ;
A79: ii `11 = o by MCART_1:85
.= ii `12 by MCART_1:85 ;
 gg `12 = ii `11 by A78;
then A80: [ii,gg] in dom (commaComp (F,G)) by A66;
hence i (*) g = (commaComp (F,G)) . (i,g) by CAT_1:def_1
.= ii * gg by A80, Def4
.= [[(gg `11),(gg `12)],[((ii `21) (*) (gg `21)),((ii `22) (*) (gg `22))]] by A1, A79, Def3, A78
.= [[(gg `11),(gg `12)],[(gg `21),((ii `22) (*) (gg `22))]] by A76, CAT_1:21, A67
.= [[(gg `11),(gg `12)],[(gg `21),(gg `22)]] by CAT_1:21, A68, A77
.= g by A69, A70, A71, A72, A63 ;
::_thesis: verum
end;
end;
A81: for f, g being Morphism of CatStr(# O,M,D9,C9,a9 #) st dom g = cod f holds
( dom (g (*) f) = dom f & cod (g (*) f) = cod g )
proof
let f, g be Morphism of CatStr(# O,M,D9,C9,a9 #); ::_thesis: ( dom g = cod f implies ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) )
assume A82: dom g = cod f ; ::_thesis: ( dom (g (*) f) = dom f & cod (g (*) f) = cod g )
reconsider f1 = f, g1 = g as Element of commaMorphs (F,G) ;
A83: ( dom g = g1 `11 & cod f = f1 `12 ) by A2, A3;
then  [g1,f1] in dom a9 by A4, A82;
then A84: ( g (*) f = a9 . (g,f) & a9 . (g1,f1) = g1 * f1 ) by Def4, CAT_1:def_1;
A85: ( dom f = f `11 & cod g = g `12 ) by A2, A3;
A86: ( dom (g (*) f) = (g (*) f) `11 & cod (g (*) f) = (g (*) f) `12 ) by A2, A3;
 g1 * f1 = [[(f1 `11),(g1 `12)],[((g1 `21) (*) (f1 `21)),((g1 `22) (*) (f1 `22))]] by A1, A82, A83, Def3;
hence  ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) by A86, A85, A84, MCART_1:85; ::_thesis: verum
end;
A87: for f, g, h being Morphism of CatStr(# O,M,D9,C9,a9 #) st dom h = cod g & dom g = cod f holds
h (*) (g (*) f) = (h (*) g) (*) f
proof
let f, g, h be Morphism of CatStr(# O,M,D9,C9,a9 #); ::_thesis: ( dom h = cod g & dom g = cod f implies h (*) (g (*) f) = (h (*) g) (*) f )
reconsider f1 = f, g1 = g, h1 = h, gf = g (*) f, hg = h (*) g as Element of commaMorphs (F,G) ;
assume that
A88: dom h = cod g and
A89: dom g = cod f ; ::_thesis: h (*) (g (*) f) = (h (*) g) (*) f
A90: ( dom g = g `11 & cod g = g `12 ) by A2, A3;
 dom (h (*) g) = dom g by A81, A88;
then A91: (h (*) g) (*) f = [[(f `11),(hg `12)],[((hg `21) (*) (f1 `21)),((hg `22) (*) (f1 `22))]] by A5, A89;
A92: ( dom h = h `11 & cod f = f `12 ) by A2, A3;
 cod (g (*) f) = cod g by A81, A89;
then A93: h (*) (g (*) f) = [[(gf `11),(h `12)],[((h1 `21) (*) (gf `21)),((h1 `22) (*) (gf `22))]] by A5, A88;
A94: ( dom (h1 `21) = (h1 `11) `11 & cod (f1 `21) = (f1 `12) `11 ) by A1, Th2;
A95: ( dom (h1 `22) = (h1 `11) `12 & cod (f1 `22) = (f1 `12) `12 ) by A1, Th2;
A96: ( dom (g1 `22) = (g1 `11) `12 & cod (g1 `22) = (g1 `12) `12 ) by A1, Th2;
A97: h (*) g = [[(g `11),(h `12)],[((h1 `21) (*) (g1 `21)),((h1 `22) (*) (g1 `22))]] by A5, A88;
then A98: ( (h (*) g) `12 = h `12 & hg `21 = (h1 `21) (*) (g1 `21) ) by MCART_1:85;
A99: g (*) f = [[(f `11),(g `12)],[((g1 `21) (*) (f1 `21)),((g1 `22) (*) (f1 `22))]] by A5, A89;
then A100: ( (g (*) f) `11 = f `11 & gf `21 = (g1 `21) (*) (f1 `21) ) by MCART_1:85;
A101: gf `22 = (g1 `22) (*) (f1 `22) by A99, MCART_1:85;
A102: hg `22 = (h1 `22) (*) (g1 `22) by A97, MCART_1:85;
 ( dom (g1 `21) = (g1 `11) `11 & cod (g1 `21) = (g1 `12) `11 ) by A1, Th2;
then  ((h1 `21) (*) (g1 `21)) (*) (f1 `21) = (h1 `21) (*) ((g1 `21) (*) (f1 `21)) by A88, A89, A90, A94, A92, CAT_1:18;
hence  h (*) (g (*) f) = (h (*) g) (*) f by A88, A89, A90, A92, A96, A95, A93, A91, A98, A100, A102, A101, CAT_1:18; ::_thesis: verum
end;
 for f, g being Morphism of CatStr(# O,M,D9,C9,a9 #) holds
( [g,f] in dom the Comp of CatStr(# O,M,D9,C9,a9 #) iff dom g = cod f )
proof
let f, g be Morphism of CatStr(# O,M,D9,C9,a9 #); ::_thesis: ( [g,f] in dom the Comp of CatStr(# O,M,D9,C9,a9 #) iff dom g = cod f )
reconsider f1 = f, g1 = g as Element of commaMorphs (F,G) ;
A103: ( dom g = g1 `11 & cod f = f1 `12 ) by A2, A3;
thus  ( [g,f] in dom the Comp of CatStr(# O,M,D9,C9,a9 #) implies dom g = cod f ) ::_thesis: ( dom g = cod f implies [g,f] in dom the Comp of CatStr(# O,M,D9,C9,a9 #) )
proof
assume  [g,f] in dom the Comp of CatStr(# O,M,D9,C9,a9 #) ; ::_thesis: dom g = cod f
then consider k1, k2 being Element of commaMorphs (F,G) such that
A104: [g,f] = [k1,k2] and
A105: k1 `11 = k2 `12 by A4;
 g = k1 by A104, XTUPLE_0:1;
hence  dom g = cod f by A103, A104, A105, XTUPLE_0:1; ::_thesis: verum
end;
thus  ( dom g = cod f implies [g,f] in dom the Comp of CatStr(# O,M,D9,C9,a9 #) ) by A4, A103; ::_thesis: verum
end;
then reconsider FG = CatStr(# O,M,D9,C9,a9 #) as strict Category by A81, A87, A11, A26, CAT_1:def_6, CAT_1:def_7, CAT_1:def_8, CAT_1:def_9, CAT_1:def_10;
take  FG ; ::_thesis: ( the carrier of FG = commaObjs (F,G) & the carrier' of FG = commaMorphs (F,G) & ( for k being Element of commaMorphs (F,G) holds the Source of FG . k = k `11 ) & ( for k being Element of commaMorphs (F,G) holds the Target of FG . k = k `12 ) & the Comp of FG = commaComp (F,G) )
thus  ( the carrier of FG = commaObjs (F,G) & the carrier' of FG = commaMorphs (F,G) & ( for k being Element of commaMorphs (F,G) holds the Source of FG . k = k `11 ) & ( for k being Element of commaMorphs (F,G) holds the Target of FG . k = k `12 ) & the Comp of FG = commaComp (F,G) ) by A2, A3; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict Category st the carrier of b1 = commaObjs (F,G) & the carrier' of b1 = commaMorphs (F,G) & ( for k being Element of commaMorphs (F,G) holds the Source of b1 . k = k `11 ) & ( for k being Element of commaMorphs (F,G) holds the Target of b1 . k = k `12 ) & the Comp of b1 = commaComp (F,G) & the carrier of b2 = commaObjs (F,G) & the carrier' of b2 = commaMorphs (F,G) & ( for k being Element of commaMorphs (F,G) holds the Source of b2 . k = k `11 ) & ( for k being Element of commaMorphs (F,G) holds the Target of b2 . k = k `12 ) & the Comp of b2 = commaComp (F,G) holds
b1 = b2
proof
let E1, E2 be strict Category; ::_thesis: ( the carrier of E1 = commaObjs (F,G) & the carrier' of E1 = commaMorphs (F,G) & ( for k being Element of commaMorphs (F,G) holds the Source of E1 . k = k `11 ) & ( for k being Element of commaMorphs (F,G) holds the Target of E1 . k = k `12 ) & the Comp of E1 = commaComp (F,G) & the carrier of E2 = commaObjs (F,G) & the carrier' of E2 = commaMorphs (F,G) & ( for k being Element of commaMorphs (F,G) holds the Source of E2 . k = k `11 ) & ( for k being Element of commaMorphs (F,G) holds the Target of E2 . k = k `12 ) & the Comp of E2 = commaComp (F,G) implies E1 = E2 )
assume that
A106: the carrier of E1 = commaObjs (F,G) and
A107: the carrier' of E1 = commaMorphs (F,G) and
A108: for k being Element of commaMorphs (F,G) holds the Source of E1 . k = k `11 and
A109: for k being Element of commaMorphs (F,G) holds the Target of E1 . k = k `12 and
A110: the Comp of E1 = commaComp (F,G) and
A111: ( the carrier of E2 = commaObjs (F,G) & the carrier' of E2 = commaMorphs (F,G) ) and
A112: for k being Element of commaMorphs (F,G) holds the Source of E2 . k = k `11 and
A113: for k being Element of commaMorphs (F,G) holds the Target of E2 . k = k `12 and
A114: the Comp of E2 = commaComp (F,G) ; ::_thesis: E1 = E2
now__::_thesis:_for_x_being_Element_of_H2(E1)_holds_the_Target_of_E1_._x_=_the_Target_of_E2_._x
let x be Element of H2(E1); ::_thesis: the Target of E1 . x = the Target of E2 . x
thus  the Target of E1 . x = x `12 by A107, A109
.= the Target of E2 . x by A107, A113 ; ::_thesis: verum
end;
then A115: the Target of E1 = the Target of E2 by A106, A107, A111, FUNCT_2:63;
now__::_thesis:_for_x_being_Element_of_H2(E1)_holds_the_Source_of_E1_._x_=_the_Source_of_E2_._x
let x be Element of H2(E1); ::_thesis: the Source of E1 . x = the Source of E2 . x
thus  the Source of E1 . x = x `11 by A107, A108
.= the Source of E2 . x by A107, A112 ; ::_thesis: verum
end;
then  the Source of E1 = the Source of E2 by A106, A107, A111, FUNCT_2:63;
hence  E1 = E2 by A106, A107, A110, A111, A114, A115; ::_thesis: verum
end;
end;

:: deftheorem  defines comma COMMACAT:def_5_:_
 for C, D, E being Category
for F being Functor of C,E
for G being Functor of D,E st ex c1 being Object of C ex d1 being Object of D ex f1 being Morphism of E st f1 in Hom ((F . c1),(G . d1)) holds
for b6 being strict Category holds
( b6 = F comma G iff ( the carrier of b6 = commaObjs (F,G) & the carrier' of b6 = commaMorphs (F,G) & ( for k being Element of commaMorphs (F,G) holds the Source of b6 . k = k `11 ) & ( for k being Element of commaMorphs (F,G) holds the Target of b6 . k = k `12 ) & the Comp of b6 = commaComp (F,G) ) );

theorem :: COMMACAT:3
for y, x being set holds
( the carrier of (1Cat (x,y)) = {x} & the carrier' of (1Cat (x,y)) = {y} ) ;

theorem Th4: :: COMMACAT:4
for y, x being set
for a, b being Object of (1Cat (x,y)) holds Hom (a,b) = {y}
proof
let y, x be set ; ::_thesis: for a, b being Object of (1Cat (x,y)) holds Hom (a,b) = {y}
let a, b be Object of (1Cat (x,y)); ::_thesis: Hom (a,b) = {y}
thus  Hom (a,b) c= {y} ; :: according to XBOOLE_0:def_10 ::_thesis: {y} c= Hom (a,b)
 y is Morphism of (1Cat (x,y)) by TARSKI:def_1;
then  y in Hom (a,b) by CAT_1:11;
hence  {y} c= Hom (a,b) by ZFMISC_1:31; ::_thesis: verum
end;

definition
let C be Category;
let c be Object of C;
func 1Cat c ->  strict Subcategory of C equals :: COMMACAT:def 6
 1Cat (c,(id c));
coherence
 1Cat (c,(id c)) is strict Subcategory of C
proof
A1: now__::_thesis:_for_a_being_Object_of_(1Cat_(c,(id_c)))
for_c1_being_Object_of_C_st_a_=_c1_holds_
id_a_=_id_c1
let a be Object of (1Cat (c,(id c))); ::_thesis: for c1 being Object of C st a = c1 holds
id a = id c1
 id a = id c by TARSKI:def_1;
hence  for c1 being Object of C st a = c1 holds
id a = id c1 by TARSKI:def_1; ::_thesis: verum
end;
A2: now__::_thesis:_for_a,_b_being_Object_of_(1Cat_(c,(id_c)))
for_c1,_c2_being_Object_of_C_st_a_=_c1_&_b_=_c2_holds_
Hom_(a,b)_c=_Hom_(c1,c2)
let a, b be Object of (1Cat (c,(id c))); ::_thesis: for c1, c2 being Object of C st a = c1 & b = c2 holds
Hom (a,b) c= Hom (c1,c2)
A3: ( a = c & b = c ) by TARSKI:def_1;
 ( id c in Hom (c,c) & Hom (a,a) = {(id c)} ) by Th4, CAT_1:27;
hence  for c1, c2 being Object of C st a = c1 & b = c2 holds
Hom (a,b) c= Hom (c1,c2) by A3, ZFMISC_1:31; ::_thesis: verum
end;
set m = id c;
set s = ((id c),(id c)) .--> (id c);
A4: dom (((id c),(id c)) .--> (id c)) = {[(id c),(id c)]} by FUNCOP_1:13;
A5: dom (id c) = c ;
A6: cod (id c) = c ;
A7: (((id c),(id c)) .--> (id c)) . ((id c),(id c)) = id c by FUNCOP_1:71;
A8: now__::_thesis:_for_x_being_set_st_x_in_dom_the_Comp_of_(1Cat_(c,(id_c)))_holds_
the_Comp_of_(1Cat_(c,(id_c)))_._x_=_the_Comp_of_C_._x
let x be set ; ::_thesis: ( x in dom the Comp of (1Cat (c,(id c))) implies the Comp of (1Cat (c,(id c))) . x = the Comp of C . x )
assume A9: x in dom the Comp of (1Cat (c,(id c))) ; ::_thesis: the Comp of (1Cat (c,(id c))) . x = the Comp of C . x
hence  the Comp of (1Cat (c,(id c))) . x = id c by A7, A4, TARSKI:def_1
.= (id c) (*) (id c) by A6, CAT_1:21
.= the Comp of C . ((id c),(id c)) by A5, A6, CAT_1:16
.= the Comp of C . x by A4, A9, TARSKI:def_1 ;
::_thesis: verum
end;
 [(id c),(id c)] in dom the Comp of C by A5, A6, CAT_1:15;
then  dom the Comp of (1Cat (c,(id c))) c= dom the Comp of C by A4, ZFMISC_1:31;
then  ( H1( 1Cat (c,(id c))) = {c} & the Comp of (1Cat (c,(id c))) c= the Comp of C ) by A8, GRFUNC_1:2;
hence  1Cat (c,(id c)) is strict Subcategory of C by A2, A1, CAT_2:def_4; ::_thesis: verum
end;
end;

:: deftheorem  defines 1Cat COMMACAT:def_6_:_
 for C being Category
for c being Object of C holds 1Cat c = 1Cat (c,(id c));

definition
let C be Category;
let c be Object of C;
funcc comma C ->  strict Category equals :: COMMACAT:def 7
(incl (1Cat c)) comma (id C);
coherence
 (incl (1Cat c)) comma (id C) is strict Category ;
funcC comma c ->  strict Category equals :: COMMACAT:def 8
(id C) comma (incl (1Cat c));
coherence
 (id C) comma (incl (1Cat c)) is strict Category ;
end;

:: deftheorem  defines comma COMMACAT:def_7_:_
 for C being Category
for c being Object of C holds c comma C = (incl (1Cat c)) comma (id C);

:: deftheorem  defines comma COMMACAT:def_8_:_
 for C being Category
for c being Object of C holds C comma c = (id C) comma (incl (1Cat c));