:: CAT_1 semantic presentation

begin

definition
attrc1 is strict ;
struct CatStr  ->  MultiGraphStruct ;
aggrCatStr(# carrier, carrier', Source, Target, Comp #) ->  CatStr ;
sel Comp c1 ->  PartFunc of [: the carrier' of c1, the carrier' of c1:], the carrier' of c1;
end;

definition
let C be CatStr ;
mode Object of C is Element of C;
mode Morphism of C is Element of the carrier' of C;
end;


registration
cluster non empty non void for CatStr ;
existence
 ex b1 being CatStr st
( not b1 is void & not b1 is empty )
proof
take  CatStr(# {0},{1},(1 :-> 0),(1 :-> 0),((1,1) :-> 1) #) ; ::_thesis: ( not CatStr(# {0},{1},(1 :-> 0),(1 :-> 0),((1,1) :-> 1) #) is void & not CatStr(# {0},{1},(1 :-> 0),(1 :-> 0),((1,1) :-> 1) #) is empty )
thus  ( not CatStr(# {0},{1},(1 :-> 0),(1 :-> 0),((1,1) :-> 1) #) is void & not CatStr(# {0},{1},(1 :-> 0),(1 :-> 0),((1,1) :-> 1) #) is empty ) ; ::_thesis: verum
end;
end;

definition
let C be CatStr ;
let f, g be Morphism of C;
assume A1: [g,f] in dom the Comp of C ;
funcg (*) f ->  Morphism of C equals :Def1: :: CAT_1:def 1
 the Comp of C . (g,f);
coherence
 the Comp of C . (g,f) is Morphism of C by A1, PARTFUN1:4;
end;

:: deftheorem Def1 defines (*) CAT_1:def_1_:_
 for C being CatStr
for f, g being Morphism of C st [g,f] in dom the Comp of C holds
g (*) f = the Comp of C . (g,f);

definition
canceled;
canceled;
let C be non empty non void CatStr ;
let a, b be Object of C;
func Hom (a,b) ->  Subset of the carrier' of C equals :: CAT_1:def 4
 {  f where f is Morphism of C : ( dom f = a & cod f = b )  }  ;
correctness
coherence
{  f where f is Morphism of C : ( dom f = a & cod f = b )  }  is Subset of the carrier' of C;
proof
set M =  {  f where f is Morphism of C : ( dom f = a & cod f = b )  }  ;
  {  f where f is Morphism of C : ( dom f = a & cod f = b )  }  c= the carrier' of C
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  f where f is Morphism of C : ( dom f = a & cod f = b )  }  or x in the carrier' of C )
assume  x in  {  f where f is Morphism of C : ( dom f = a & cod f = b )  }  ; ::_thesis: x in the carrier' of C
then  ex f being Morphism of C st
( x = f & dom f = a & cod f = b ) ;
hence  x in the carrier' of C ; ::_thesis: verum
end;
hence   {  f where f is Morphism of C : ( dom f = a & cod f = b )  }  is Subset of the carrier' of C ; ::_thesis: verum
end;
end;

:: deftheorem  CAT_1:def_2_:_
canceled;

:: deftheorem  CAT_1:def_3_:_
canceled;

:: deftheorem  defines Hom CAT_1:def_4_:_
 for C being non empty non void CatStr
for a, b being Object of C holds Hom (a,b) =  {  f where f is Morphism of C : ( dom f = a & cod f = b )  }  ;


theorem Th1: :: CAT_1:1
for C being non empty non void CatStr
for f being Morphism of C
for a, b being Object of C holds
( f in Hom (a,b) iff ( dom f = a & cod f = b ) )
proof
let C be non empty non void CatStr ; ::_thesis: for f being Morphism of C
for a, b being Object of C holds
( f in Hom (a,b) iff ( dom f = a & cod f = b ) )
let f be Morphism of C; ::_thesis: for a, b being Object of C holds
( f in Hom (a,b) iff ( dom f = a & cod f = b ) )
let a, b be Object of C; ::_thesis: ( f in Hom (a,b) iff ( dom f = a & cod f = b ) )
thus  ( f in Hom (a,b) implies ( dom f = a & cod f = b ) ) ::_thesis: ( dom f = a & cod f = b implies f in Hom (a,b) )
proof
assume  f in Hom (a,b) ; ::_thesis: ( dom f = a & cod f = b )
then  ex g being Morphism of C st
( f = g & dom g = a & cod g = b ) ;
hence  ( dom f = a & cod f = b ) ; ::_thesis: verum
end;
thus  ( dom f = a & cod f = b implies f in Hom (a,b) ) ; ::_thesis: verum
end;

theorem :: CAT_1:2
for C being non empty non void CatStr
for f being Morphism of C holds Hom ((dom f),(cod f)) <> {} by Th1;

definition
let C be non empty non void CatStr ;
let a, b be Object of C;
assume A1: Hom (a,b) <> {} ;
mode Morphism of a,b ->  Morphism of C means :Def4: :: CAT_1:def 5
it in Hom (a,b);
existence
 ex b1 being Morphism of C st b1 in Hom (a,b) by A1, SUBSET_1:4;
end;

:: deftheorem Def4 defines Morphism CAT_1:def_5_:_
 for C being non empty non void CatStr
for a, b being Object of C st Hom (a,b) <> {} holds
for b4 being Morphism of C holds
( b4 is Morphism of a,b iff b4 in Hom (a,b) );

theorem :: CAT_1:3
canceled;

theorem Th4: :: CAT_1:4
for C being non empty non void CatStr
for f being Morphism of C holds f is Morphism of dom f, cod f
proof
let C be non empty non void CatStr ; ::_thesis: for f being Morphism of C holds f is Morphism of dom f, cod f
let f be Morphism of C; ::_thesis: f is Morphism of dom f, cod f
 f in Hom ((dom f),(cod f)) ;
hence  f is Morphism of dom f, cod f by Def4; ::_thesis: verum
end;

theorem Th5: :: CAT_1:5
for C being non empty non void CatStr
for a, b being Object of C
for f being Morphism of a,b st Hom (a,b) <> {} holds
( dom f = a & cod f = b )
proof
let C be non empty non void CatStr ; ::_thesis: for a, b being Object of C
for f being Morphism of a,b st Hom (a,b) <> {} holds
( dom f = a & cod f = b )
let a, b be Object of C; ::_thesis: for f being Morphism of a,b st Hom (a,b) <> {} holds
( dom f = a & cod f = b )
let f be Morphism of a,b; ::_thesis: ( Hom (a,b) <> {} implies ( dom f = a & cod f = b ) )
assume  Hom (a,b) <> {} ; ::_thesis: ( dom f = a & cod f = b )
then  f in Hom (a,b) by Def4;
hence  ( dom f = a & cod f = b ) by Th1; ::_thesis: verum
end;

theorem :: CAT_1:6
for C being non empty non void CatStr
for a, b, c, d being Object of C
for f being Morphism of a,b
for h being Morphism of c,d st Hom (a,b) <> {} & Hom (c,d) <> {} & f = h holds
( a = c & b = d )
proof
let C be non empty non void CatStr ; ::_thesis: for a, b, c, d being Object of C
for f being Morphism of a,b
for h being Morphism of c,d st Hom (a,b) <> {} & Hom (c,d) <> {} & f = h holds
( a = c & b = d )
let a, b, c, d be Object of C; ::_thesis: for f being Morphism of a,b
for h being Morphism of c,d st Hom (a,b) <> {} & Hom (c,d) <> {} & f = h holds
( a = c & b = d )
let f be Morphism of a,b; ::_thesis: for h being Morphism of c,d st Hom (a,b) <> {} & Hom (c,d) <> {} & f = h holds
( a = c & b = d )
let h be Morphism of c,d; ::_thesis: ( Hom (a,b) <> {} & Hom (c,d) <> {} & f = h implies ( a = c & b = d ) )
assume that
A1: Hom (a,b) <> {} and
A2: Hom (c,d) <> {} ; ::_thesis: ( not f = h or ( a = c & b = d ) )
 ( dom f = a & cod f = b ) by A1, Th5;
hence  ( not f = h or ( a = c & b = d ) ) by A2, Th5; ::_thesis: verum
end;

theorem Th7: :: CAT_1:7
for C being non empty non void CatStr
for a, b being Object of C
for f being Morphism of a,b st Hom (a,b) = {f} holds
for g being Morphism of a,b holds f = g
proof
let C be non empty non void CatStr ; ::_thesis: for a, b being Object of C
for f being Morphism of a,b st Hom (a,b) = {f} holds
for g being Morphism of a,b holds f = g
let a, b be Object of C; ::_thesis: for f being Morphism of a,b st Hom (a,b) = {f} holds
for g being Morphism of a,b holds f = g
let f be Morphism of a,b; ::_thesis: ( Hom (a,b) = {f} implies for g being Morphism of a,b holds f = g )
assume A1: Hom (a,b) = {f} ; ::_thesis: for g being Morphism of a,b holds f = g
let g be Morphism of a,b; ::_thesis: f = g
 g in {f} by A1, Def4;
hence  f = g by TARSKI:def_1; ::_thesis: verum
end;

theorem Th8: :: CAT_1:8
for C being non empty non void CatStr
for a, b being Object of C
for f being Morphism of a,b st Hom (a,b) <> {} & ( for g being Morphism of a,b holds f = g ) holds
Hom (a,b) = {f}
proof
let C be non empty non void CatStr ; ::_thesis: for a, b being Object of C
for f being Morphism of a,b st Hom (a,b) <> {} & ( for g being Morphism of a,b holds f = g ) holds
Hom (a,b) = {f}
let a, b be Object of C; ::_thesis: for f being Morphism of a,b st Hom (a,b) <> {} & ( for g being Morphism of a,b holds f = g ) holds
Hom (a,b) = {f}
let f be Morphism of a,b; ::_thesis: ( Hom (a,b) <> {} & ( for g being Morphism of a,b holds f = g ) implies Hom (a,b) = {f} )
assume that
A1: Hom (a,b) <> {} and
A2: for g being Morphism of a,b holds f = g ; ::_thesis: Hom (a,b) = {f}
 for x being set holds
( x in Hom (a,b) iff x = f )
proof
let x be set ; ::_thesis: ( x in Hom (a,b) iff x = f )
thus  ( x in Hom (a,b) implies x = f ) ::_thesis: ( x = f implies x in Hom (a,b) )
proof
assume  x in Hom (a,b) ; ::_thesis: x = f
then consider g being Morphism of C such that
A3: x = g and
A4: ( dom g = a & cod g = b ) ;
 g is Morphism of a,b by A4, Th4;
hence  x = f by A2, A3; ::_thesis: verum
end;
thus  ( x = f implies x in Hom (a,b) ) by A1, Def4; ::_thesis: verum
end;
hence  Hom (a,b) = {f} by TARSKI:def_1; ::_thesis: verum
end;

theorem :: CAT_1:9
for C being non empty non void CatStr
for a, b, c, d being Object of C
for f being Morphism of a,b st Hom (a,b), Hom (c,d) are_equipotent & Hom (a,b) = {f} holds
ex h being Morphism of c,d st Hom (c,d) = {h}
proof
let C be non empty non void CatStr ; ::_thesis: for a, b, c, d being Object of C
for f being Morphism of a,b st Hom (a,b), Hom (c,d) are_equipotent & Hom (a,b) = {f} holds
ex h being Morphism of c,d st Hom (c,d) = {h}
let a, b, c, d be Object of C; ::_thesis: for f being Morphism of a,b st Hom (a,b), Hom (c,d) are_equipotent & Hom (a,b) = {f} holds
ex h being Morphism of c,d st Hom (c,d) = {h}
let f be Morphism of a,b; ::_thesis: ( Hom (a,b), Hom (c,d) are_equipotent & Hom (a,b) = {f} implies ex h being Morphism of c,d st Hom (c,d) = {h} )
assume  Hom (a,b), Hom (c,d) are_equipotent ; ::_thesis: ( not Hom (a,b) = {f} or ex h being Morphism of c,d st Hom (c,d) = {h} )
then consider F being Function such that
 F is one-to-one and
A1: ( dom F = Hom (a,b) & rng F = Hom (c,d) ) by WELLORD2:def_4;
assume  Hom (a,b) = {f} ; ::_thesis: ex h being Morphism of c,d st Hom (c,d) = {h}
then A2: Hom (c,d) = {(F . f)} by A1, FUNCT_1:4;
then  F . f in Hom (c,d) by TARSKI:def_1;
then  F . f is Morphism of c,d by Def4;
hence  ex h being Morphism of c,d st Hom (c,d) = {h} by A2; ::_thesis: verum
end;

definition
let C be non empty non void CatStr ;
attrC is Category-like  means :Def5a: :: CAT_1:def 6
 for f, g being Morphism of C holds
( [g,f] in dom the Comp of C iff dom g = cod f );
attrC is transitive  means :Def5b: :: CAT_1:def 7
 for f, g being Morphism of C st dom g = cod f holds
( dom (g (*) f) = dom f & cod (g (*) f) = cod g );
attrC is associative  means :Def5c: :: CAT_1:def 8
 for f, g, h being Morphism of C st dom h = cod g & dom g = cod f holds
h (*) (g (*) f) = (h (*) g) (*) f;
attrC is reflexive  means :Def5d: :: CAT_1:def 9
 for b being Element of C holds Hom (b,b) <> {} ;
attrC is with_identities  means :Def5e: :: CAT_1:def 10
 for a being Element of C ex i being Morphism of a,a st
for b being Element of C 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 ) );
end;

:: deftheorem Def5a defines Category-like CAT_1:def_6_:_
 for C being non empty non void CatStr holds
( C is Category-like iff for f, g being Morphism of C holds
( [g,f] in dom the Comp of C iff dom g = cod f ) );

:: deftheorem Def5b defines transitive CAT_1:def_7_:_
 for C being non empty non void CatStr holds
( C is transitive iff for f, g being Morphism of C st dom g = cod f holds
( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) );

:: deftheorem Def5c defines associative CAT_1:def_8_:_
 for C being non empty non void CatStr holds
( C is associative iff for f, g, h being Morphism of C st dom h = cod g & dom g = cod f holds
h (*) (g (*) f) = (h (*) g) (*) f );

:: deftheorem Def5d defines reflexive CAT_1:def_9_:_
 for C being non empty non void CatStr holds
( C is reflexive iff for b being Element of C holds Hom (b,b) <> {} );

:: deftheorem Def5e defines with_identities CAT_1:def_10_:_
 for C being non empty non void CatStr holds
( C is with_identities iff for a being Element of C ex i being Morphism of a,a st
for b being Element of C 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 ) ) );

definition
let o, m be set ;
func 1Cat (o,m) ->  strict CatStr  equals :: CAT_1:def 11
 CatStr(# {o},{m},(m :-> o),(m :-> o),((m,m) :-> m) #);
correctness
coherence
CatStr(# {o},{m},(m :-> o),(m :-> o),((m,m) :-> m) #) is strict CatStr ;
;
end;

:: deftheorem  defines 1Cat CAT_1:def_11_:_
 for o, m being set holds 1Cat (o,m) = CatStr(# {o},{m},(m :-> o),(m :-> o),((m,m) :-> m) #);

registration
let o, m be set ;
cluster 1Cat (o,m) ->  non empty trivial non void trivial' strict ;
coherence
 ( not 1Cat (o,m) is empty & 1Cat (o,m) is trivial & not 1Cat (o,m) is void & 1Cat (o,m) is trivial' ) ;
end;

registration
cluster non empty trivial non void  ->  non empty non void transitive reflexive for CatStr ;
coherence
 for b1 being non empty non void CatStr st not b1 is empty & b1 is trivial holds
( b1 is transitive & b1 is reflexive )
proof
let C be non empty non void CatStr ; ::_thesis: ( not C is empty & C is trivial implies ( C is transitive & C is reflexive ) )
assume Z: ( not C is empty & C is trivial ) ; ::_thesis: ( C is transitive & C is reflexive )
thus  for f, g being Morphism of C st dom g = cod f holds
( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) by Z, ZFMISC_1:def_10; :: according to CAT_1:def_7 ::_thesis: C is reflexive
let b be Element of C; :: according to CAT_1:def_9 ::_thesis: Hom (b,b) <> {}
set i = the Morphism of C;
 ( cod the Morphism of C = b & dom the Morphism of C = b ) by Z, ZFMISC_1:def_10;
hence  Hom (b,b) <> {} by Th1; ::_thesis: verum
end;
end;

registration
cluster non empty non void trivial'  ->  non empty non void associative with_identities for CatStr ;
coherence
 for b1 being non empty non void CatStr st not b1 is void & b1 is trivial' holds
( b1 is associative & b1 is with_identities )
proof
let C be non empty non void CatStr ; ::_thesis: ( not C is void & C is trivial' implies ( C is associative & C is with_identities ) )
assume Z: ( not C is void & C is trivial' ) ; ::_thesis: ( C is associative & C is with_identities )
thus  for f, g, h being Morphism of C st dom h = cod g & dom g = cod f holds
h (*) (g (*) f) = (h (*) g) (*) f by Z, ZFMISC_1:def_10; :: according to CAT_1:def_8 ::_thesis: C is with_identities
let a be Element of C; :: according to CAT_1:def_10 ::_thesis: ex i being Morphism of a,a st
for b being Element of C 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 ) )
take i = the Morphism of a,a; ::_thesis: for b being Element of C 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 C; ::_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 ) by Z, ZFMISC_1:def_10; ::_thesis: ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f )
thus  ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) by Z, ZFMISC_1:def_10; ::_thesis: verum
end;
end;

registration
let o, m be set ;
cluster 1Cat (o,m) ->  strict Category-like ;
coherence
 1Cat (o,m) is Category-like
proof
let f, g be Morphism of (1Cat (o,m)); :: according to CAT_1:def_6 ::_thesis: ( [g,f] in dom the Comp of (1Cat (o,m)) iff dom g = cod f )
thus  ( [g,f] in dom the Comp of (1Cat (o,m)) implies dom g = cod f ) by ZFMISC_1:def_10; ::_thesis: ( dom g = cod f implies [g,f] in dom the Comp of (1Cat (o,m)) )
assume  dom g = cod f ; ::_thesis: [g,f] in dom the Comp of (1Cat (o,m))
A2: dom the Comp of (1Cat (o,m)) = {[m,m]} by FUNCOP_1:13;
 ( f = m & g = m ) by TARSKI:def_1;
hence  [g,f] in dom the Comp of (1Cat (o,m)) by A2, TARSKI:def_1; ::_thesis: verum
end;
end;

registration
cluster non empty non void V59() strict Category-like transitive associative reflexive with_identities for CatStr ;
existence
 ex b1 being non empty non void CatStr st
( b1 is reflexive & b1 is transitive & b1 is associative & b1 is with_identities & b1 is Category-like & not b1 is void & not b1 is empty & b1 is strict )
proof
take  1Cat (0,0) ; ::_thesis: ( 1Cat (0,0) is reflexive & 1Cat (0,0) is transitive & 1Cat (0,0) is associative & 1Cat (0,0) is with_identities & 1Cat (0,0) is Category-like & not 1Cat (0,0) is void & not 1Cat (0,0) is empty & 1Cat (0,0) is strict )
thus  ( 1Cat (0,0) is reflexive & 1Cat (0,0) is transitive & 1Cat (0,0) is associative & 1Cat (0,0) is with_identities & 1Cat (0,0) is Category-like & not 1Cat (0,0) is void & not 1Cat (0,0) is empty & 1Cat (0,0) is strict ) ; ::_thesis: verum
end;
end;

definition
mode Category is non empty non void Category-like transitive associative reflexive with_identities CatStr ;
end;

registration
let C be non empty non void reflexive CatStr ;
let a be Object of C;
cluster Hom (a,a) ->  non empty ;
coherence
 not Hom (a,a) is empty by Def5d;
end;

definition
let C be non empty non void reflexive with_identities CatStr ;
let a be Object of C;
func id a ->  Morphism of a,a means :Defid: :: CAT_1:def 12
 for b being Object of C holds
( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) it = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds it (*) f = f ) );
existence
 ex b1 being Morphism of a,a st
for b being Object of C holds
( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) b1 = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds b1 (*) f = f ) ) by Def5e;
uniqueness
 for b1, b2 being Morphism of a,a st ( for b being Object of C holds
( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) b1 = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds b1 (*) f = f ) ) ) & ( for b being Object of C holds
( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) b2 = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds b2 (*) f = f ) ) ) holds
b1 = b2
proof
let m1, m2 be Morphism of a,a; ::_thesis: ( ( for b being Object of C holds
( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) m1 = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds m1 (*) f = f ) ) ) & ( for b being Object of C holds
( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) m2 = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds m2 (*) f = f ) ) ) implies m1 = m2 )
assume that
Z1: for b being Object of C holds
( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) m1 = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds m1 (*) f = f ) ) and
Z2: for b being Object of C holds
( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) m2 = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds m2 (*) f = f ) ) ; ::_thesis: m1 = m2
A: Hom (a,a) <> {} ;
hence m1 = m1 (*) m2 by Z2
.= m2 by A, Z1 ;
::_thesis: verum
end;
end;

:: deftheorem Defid defines id CAT_1:def_12_:_
 for C being non empty non void reflexive with_identities CatStr
for a being Object of C
for b3 being Morphism of a,a holds
( b3 = id a iff for b being Object of C holds
( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) b3 = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds b3 (*) f = f ) ) );

theorem :: CAT_1:10
canceled;


theorem Th11: :: CAT_1:11
for o, m being set
for a, b being Object of (1Cat (o,m))
for f being Morphism of (1Cat (o,m)) holds f in Hom (a,b)
proof
let o, m be set ; ::_thesis: for a, b being Object of (1Cat (o,m))
for f being Morphism of (1Cat (o,m)) holds f in Hom (a,b)
let a, b be Object of (1Cat (o,m)); ::_thesis: for f being Morphism of (1Cat (o,m)) holds f in Hom (a,b)
let f be Morphism of (1Cat (o,m)); ::_thesis: f in Hom (a,b)
 dom f = o by TARSKI:def_1;
then  ( dom f = a & cod f = b ) by TARSKI:def_1;
hence  f in Hom (a,b) ; ::_thesis: verum
end;

theorem :: CAT_1:12
for o, m being set
for a, b being Object of (1Cat (o,m))
for f being Morphism of (1Cat (o,m)) holds f is Morphism of a,b
proof
let o, m be set ; ::_thesis: for a, b being Object of (1Cat (o,m))
for f being Morphism of (1Cat (o,m)) holds f is Morphism of a,b
let a, b be Object of (1Cat (o,m)); ::_thesis: for f being Morphism of (1Cat (o,m)) holds f is Morphism of a,b
let f be Morphism of (1Cat (o,m)); ::_thesis: f is Morphism of a,b
 f in Hom (a,b) by Th11;
hence  f is Morphism of a,b by Def4; ::_thesis: verum
end;

theorem :: CAT_1:13
for o, m being set
for a, b being Object of (1Cat (o,m)) holds Hom (a,b) <> {} by Th11;

theorem :: CAT_1:14
for o, m being set
for a, b, c, d being Object of (1Cat (o,m))
for f being Morphism of a,b
for g being Morphism of c,d holds f = g
proof
let o, m be set ; ::_thesis: for a, b, c, d being Object of (1Cat (o,m))
for f being Morphism of a,b
for g being Morphism of c,d holds f = g
let a, b, c, d be Object of (1Cat (o,m)); ::_thesis: for f being Morphism of a,b
for g being Morphism of c,d holds f = g
let f be Morphism of a,b; ::_thesis: for g being Morphism of c,d holds f = g
let g be Morphism of c,d; ::_thesis: f = g
 f = m by TARSKI:def_1;
hence  f = g by TARSKI:def_1; ::_thesis: verum
end;


theorem :: CAT_1:15
for C being Category
for g, f being Morphism of C holds
( dom g = cod f iff [g,f] in dom the Comp of C ) by Def5a;

theorem Th16: :: CAT_1:16
for C being Category
for g, f being Morphism of C st dom g = cod f holds
g (*) f = the Comp of C . (g,f)
proof
let C be Category; ::_thesis: for g, f being Morphism of C st dom g = cod f holds
g (*) f = the Comp of C . (g,f)
let g, f be Morphism of C; ::_thesis: ( dom g = cod f implies g (*) f = the Comp of C . (g,f) )
assume  dom g = cod f ; ::_thesis: g (*) f = the Comp of C . (g,f)
then  [g,f] in dom the Comp of C by Def5a;
hence  g (*) f = the Comp of C . (g,f) by Def1; ::_thesis: verum
end;

theorem :: CAT_1:17
for C being Category
for f, g being Morphism of C st dom g = cod f holds
( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) by Def5b;

theorem :: CAT_1:18
for C being Category
for f, g, h being Morphism of C st dom h = cod g & dom g = cod f holds
h (*) (g (*) f) = (h (*) g) (*) f by Def5c;

theorem :: CAT_1:19
canceled;

theorem :: CAT_1:20
canceled;

theorem :: CAT_1:21
for C being Category
for b being Object of C
for f being Morphism of C st cod f = b holds
(id b) (*) f = f
proof
let C be Category; ::_thesis: for b being Object of C
for f being Morphism of C st cod f = b holds
(id b) (*) f = f
let b be Object of C; ::_thesis: for f being Morphism of C st cod f = b holds
(id b) (*) f = f
let f be Morphism of C; ::_thesis: ( cod f = b implies (id b) (*) f = f )
assume Z: cod f = b ; ::_thesis: (id b) (*) f = f
then reconsider ff = f as Morphism of dom f,b by Th4;
 Hom ((dom f),b) <> {} by Z, Th1;
then  (id b) (*) ff = ff by Defid;
hence  (id b) (*) f = f ; ::_thesis: verum
end;

theorem :: CAT_1:22
for C being Category
for b being Object of C
for g being Morphism of C st dom g = b holds
g (*) (id b) = g
proof
let C be Category; ::_thesis: for b being Object of C
for g being Morphism of C st dom g = b holds
g (*) (id b) = g
let b be Object of C; ::_thesis: for g being Morphism of C st dom g = b holds
g (*) (id b) = g
let f be Morphism of C; ::_thesis: ( dom f = b implies f (*) (id b) = f )
assume Z: dom f = b ; ::_thesis: f (*) (id b) = f
then reconsider ff = f as Morphism of b, cod f by Th4;
 Hom (b,(cod f)) <> {} by Z, Th1;
then  ff (*) (id b) = ff by Defid;
hence  f (*) (id b) = f ; ::_thesis: verum
end;


theorem Th23: :: CAT_1:23
for C being Category
for a, b, c being Object of C
for f being Morphism of a,b
for g being Morphism of b,c st Hom (a,b) <> {} & Hom (b,c) <> {} holds
g (*) f in Hom (a,c)
proof
let C be Category; ::_thesis: for a, b, c being Object of C
for f being Morphism of a,b
for g being Morphism of b,c st Hom (a,b) <> {} & Hom (b,c) <> {} holds
g (*) f in Hom (a,c)
let a, b, c be Object of C; ::_thesis: for f being Morphism of a,b
for g being Morphism of b,c st Hom (a,b) <> {} & Hom (b,c) <> {} holds
g (*) f in Hom (a,c)
let f be Morphism of a,b; ::_thesis: for g being Morphism of b,c st Hom (a,b) <> {} & Hom (b,c) <> {} holds
g (*) f in Hom (a,c)
let g be Morphism of b,c; ::_thesis: ( Hom (a,b) <> {} & Hom (b,c) <> {} implies g (*) f in Hom (a,c) )
assume that
A1: Hom (a,b) <> {} and
A2: Hom (b,c) <> {} ; ::_thesis: g (*) f in Hom (a,c)
A3: f in Hom (a,b) by A1, Def4;
then A4: cod f = b by Th1;
A5: g in Hom (b,c) by A2, Def4;
then A6: dom g = b by Th1;
 cod g = c by A5, Th1;
then A7: cod (g (*) f) = c by A6, A4, Def5b;
 dom f = a by A3, Th1;
then  dom (g (*) f) = a by A6, A4, Def5b;
hence  g (*) f in Hom (a,c) by A7; ::_thesis: verum
end;

definition
let C be Category;
let a, b, c be Object of C;
let f be Morphism of a,b;
let g be Morphism of b,c;
assume A1: ( Hom (a,b) <> {} & Hom (b,c) <> {} ) ;
funcg * f ->  Morphism of a,c equals :Def10: :: CAT_1:def 13
g (*) f;
correctness
coherence
g (*) f is Morphism of a,c;
proof
 g (*) f in Hom (a,c) by A1, Th23;
hence  g (*) f is Morphism of a,c by Def4; ::_thesis: verum
end;
end;

:: deftheorem Def10 defines * CAT_1:def_13_:_
 for C being Category
for a, b, c being Object of C
for f being Morphism of a,b
for g being Morphism of b,c st Hom (a,b) <> {} & Hom (b,c) <> {} holds
g * f = g (*) f;

theorem :: CAT_1:24
for C being Category
for a, b, c being Object of C st Hom (a,b) <> {} & Hom (b,c) <> {} holds
Hom (a,c) <> {} by Th23;

theorem Th25: :: CAT_1:25
for C being Category
for a, b, c, d being Object of C
for f being Morphism of a,b
for g being Morphism of b,c
for h being Morphism of c,d st Hom (a,b) <> {} & Hom (b,c) <> {} & Hom (c,d) <> {} holds
(h * g) * f = h * (g * f)
proof
let C be Category; ::_thesis: for a, b, c, d being Object of C
for f being Morphism of a,b
for g being Morphism of b,c
for h being Morphism of c,d st Hom (a,b) <> {} & Hom (b,c) <> {} & Hom (c,d) <> {} holds
(h * g) * f = h * (g * f)
let a, b, c, d be Object of C; ::_thesis: for f being Morphism of a,b
for g being Morphism of b,c
for h being Morphism of c,d st Hom (a,b) <> {} & Hom (b,c) <> {} & Hom (c,d) <> {} holds
(h * g) * f = h * (g * f)
let f be Morphism of a,b; ::_thesis: for g being Morphism of b,c
for h being Morphism of c,d st Hom (a,b) <> {} & Hom (b,c) <> {} & Hom (c,d) <> {} holds
(h * g) * f = h * (g * f)
let g be Morphism of b,c; ::_thesis: for h being Morphism of c,d st Hom (a,b) <> {} & Hom (b,c) <> {} & Hom (c,d) <> {} holds
(h * g) * f = h * (g * f)
let h be Morphism of c,d; ::_thesis: ( Hom (a,b) <> {} & Hom (b,c) <> {} & Hom (c,d) <> {} implies (h * g) * f = h * (g * f) )
assume that
A1: Hom (a,b) <> {} and
A2: Hom (b,c) <> {} and
A3: Hom (c,d) <> {} ; ::_thesis: (h * g) * f = h * (g * f)
A4: Hom (a,c) <> {} by A1, A2, Th23;
 h in Hom (c,d) by A3, Def4;
then A5: dom h = c by Th1;
 g in Hom (b,c) by A2, Def4;
then A6: ( cod g = c & dom g = b ) by Th1;
reconsider hh = h as Morphism of C ;
reconsider gg = g as Morphism of C ;
reconsider ff = f as Morphism of C ;
 f in Hom (a,b) by A1, Def4;
then A7: cod f = b by Th1;
 Hom (b,d) <> {} by A2, A3, Th23;
hence (h * g) * f = (h * g) (*) ff by A1, Def10
.= (hh (*) gg) (*) ff by A2, A3, Def10
.= hh (*) (gg (*) ff) by A5, A6, A7, Def5c
.= hh (*) (g * f) by A1, A2, Def10
.= h * (g * f) by A3, A4, Def10 ;
::_thesis: verum
end;

theorem :: CAT_1:26
canceled;

theorem :: CAT_1:27
for C being Category
for a being Object of C holds id a in Hom (a,a) by Def4;

theorem Th28: :: CAT_1:28
for C being Category
for a, b being Object of C
for f being Morphism of a,b st Hom (a,b) <> {} holds
(id b) * f = f
proof
let C be Category; ::_thesis: for a, b being Object of C
for f being Morphism of a,b st Hom (a,b) <> {} holds
(id b) * f = f
let a, b be Object of C; ::_thesis: for f being Morphism of a,b st Hom (a,b) <> {} holds
(id b) * f = f
let f be Morphism of a,b; ::_thesis: ( Hom (a,b) <> {} implies (id b) * f = f )
assume A1: Hom (a,b) <> {} ; ::_thesis: (id b) * f = f
A2: (id b) (*) f = f by A1, Defid;
 Hom (b,b) <> {} ;
hence  (id b) * f = f by A1, A2, Def10; ::_thesis: verum
end;

theorem Th29: :: CAT_1:29
for C being Category
for b, c being Object of C
for g being Morphism of b,c st Hom (b,c) <> {} holds
g * (id b) = g
proof
let C be Category; ::_thesis: for b, c being Object of C
for g being Morphism of b,c st Hom (b,c) <> {} holds
g * (id b) = g
let b, c be Object of C; ::_thesis: for g being Morphism of b,c st Hom (b,c) <> {} holds
g * (id b) = g
let g be Morphism of b,c; ::_thesis: ( Hom (b,c) <> {} implies g * (id b) = g )
assume A1: Hom (b,c) <> {} ; ::_thesis: g * (id b) = g
A2: g (*) (id b) = g by A1, Defid;
 Hom (b,b) <> {} ;
hence  g * (id b) = g by A1, A2, Def10; ::_thesis: verum
end;

registration
let C be Category;
let a be Object of C;
let f be Morphism of a,a;
X: Hom (a,a) <> {} ;
reducef * (id a) to f;
reducibility
 f * (id a) = f by X, Th29;
reduce(id a) * f to f;
reducibility
 (id a) * f = f by X, Th28;
end;

theorem :: CAT_1:30
for C being Category
for a being Object of C holds (id a) * (id a) = id a ;

definition
let C be Category;
let b, c be Object of C;
let g be Morphism of b,c;
attrg is monic  means :Defm: :: CAT_1:def 14
( Hom (b,c) <> {} & ( for a being Object of C st Hom (a,b) <> {} holds
for f1, f2 being Morphism of a,b st g * f1 = g * f2 holds
f1 = f2 ) );
end;

:: deftheorem Defm defines monic CAT_1:def_14_:_
 for C being Category
for b, c being Object of C
for g being Morphism of b,c holds
( g is monic iff ( Hom (b,c) <> {} & ( for a being Object of C st Hom (a,b) <> {} holds
for f1, f2 being Morphism of a,b st g * f1 = g * f2 holds
f1 = f2 ) ) );

definition
let C be Category;
let a, b be Object of C;
let f be Morphism of a,b;
attrf is epi  means :Defe: :: CAT_1:def 15
( Hom (a,b) <> {} & ( for c being Object of C st Hom (b,c) <> {} holds
for g1, g2 being Morphism of b,c st g1 * f = g2 * f holds
g1 = g2 ) );
end;

:: deftheorem Defe defines epi CAT_1:def_15_:_
 for C being Category
for a, b being Object of C
for f being Morphism of a,b holds
( f is epi iff ( Hom (a,b) <> {} & ( for c being Object of C st Hom (b,c) <> {} holds
for g1, g2 being Morphism of b,c st g1 * f = g2 * f holds
g1 = g2 ) ) );

definition
let C be Category;
let a, b be Object of C;
let f be Morphism of a,b;
attrf is invertible  means :Dfi: :: CAT_1:def 16
( Hom (a,b) <> {} & Hom (b,a) <> {} & ex g being Morphism of b,a st
( f * g = id b & g * f = id a ) );
end;

:: deftheorem Dfi defines invertible CAT_1:def_16_:_
 for C being Category
for a, b being Object of C
for f being Morphism of a,b holds
( f is invertible iff ( Hom (a,b) <> {} & Hom (b,a) <> {} & ex g being Morphism of b,a st
( f * g = id b & g * f = id a ) ) );

theorem Th31: :: CAT_1:31
for C being Category
for b, c being Object of C
for g being Morphism of b,c st Hom (b,c) <> {} holds
( g is monic iff for a being Object of C
for f1, f2 being Morphism of a,b st Hom (a,b) <> {} & g * f1 = g * f2 holds
f1 = f2 )
proof
let C be Category; ::_thesis: for b, c being Object of C
for g being Morphism of b,c st Hom (b,c) <> {} holds
( g is monic iff for a being Object of C
for f1, f2 being Morphism of a,b st Hom (a,b) <> {} & g * f1 = g * f2 holds
f1 = f2 )
let b, c be Object of C; ::_thesis: for g being Morphism of b,c st Hom (b,c) <> {} holds
( g is monic iff for a being Object of C
for f1, f2 being Morphism of a,b st Hom (a,b) <> {} & g * f1 = g * f2 holds
f1 = f2 )
let g be Morphism of b,c; ::_thesis: ( Hom (b,c) <> {} implies ( g is monic iff for a being Object of C
for f1, f2 being Morphism of a,b st Hom (a,b) <> {} & g * f1 = g * f2 holds
f1 = f2 ) )
assume A1: Hom (b,c) <> {} ; ::_thesis: ( g is monic iff for a being Object of C
for f1, f2 being Morphism of a,b st Hom (a,b) <> {} & g * f1 = g * f2 holds
f1 = f2 )
thus  ( g is monic implies for a being Object of C
for f1, f2 being Morphism of a,b st Hom (a,b) <> {} & g * f1 = g * f2 holds
f1 = f2 ) by Defm; ::_thesis: ( ( for a being Object of C
for f1, f2 being Morphism of a,b st Hom (a,b) <> {} & g * f1 = g * f2 holds
f1 = f2 ) implies g is monic )
assume A7: for a being Object of C
for f1, f2 being Morphism of a,b st Hom (a,b) <> {} & g * f1 = g * f2 holds
f1 = f2 ; ::_thesis: g is monic
thus  Hom (b,c) <> {} by A1; :: according to CAT_1:def_14 ::_thesis: for a being Object of C st Hom (a,b) <> {} holds
for f1, f2 being Morphism of a,b st g * f1 = g * f2 holds
f1 = f2
thus  for a being Object of C st Hom (a,b) <> {} holds
for f1, f2 being Morphism of a,b st g * f1 = g * f2 holds
f1 = f2 by A7; ::_thesis: verum
end;

theorem :: CAT_1:32
for C being Category
for b, c, d being Object of C
for g being Morphism of b,c
for h being Morphism of c,d st g is monic & h is monic holds
h * g is monic
proof
let C be Category; ::_thesis: for b, c, d being Object of C
for g being Morphism of b,c
for h being Morphism of c,d st g is monic & h is monic holds
h * g is monic
let b, c, d be Object of C; ::_thesis: for g being Morphism of b,c
for h being Morphism of c,d st g is monic & h is monic holds
h * g is monic
let g be Morphism of b,c; ::_thesis: for h being Morphism of c,d st g is monic & h is monic holds
h * g is monic
let h be Morphism of c,d; ::_thesis: ( g is monic & h is monic implies h * g is monic )
assume that
A3: g is monic and
A4: h is monic ; ::_thesis: h * g is monic
A1: Hom (b,c) <> {} by A3, Defm;
A2: Hom (c,d) <> {} by A4, Defm;
A5: now__::_thesis:_for_a_being_Object_of_C
for_f1,_f2_being_Morphism_of_a,b_st_Hom_(a,b)_<>_{}_&_(h_*_g)_*_f1_=_(h_*_g)_*_f2_holds_
f1_=_f2
let a be Object of C; ::_thesis: for f1, f2 being Morphism of a,b st Hom (a,b) <> {} & (h * g) * f1 = (h * g) * f2 holds
f1 = f2
let f1, f2 be Morphism of a,b; ::_thesis: ( Hom (a,b) <> {} & (h * g) * f1 = (h * g) * f2 implies f1 = f2 )
assume that
A6: Hom (a,b) <> {} and
A7: (h * g) * f1 = (h * g) * f2 ; ::_thesis: f1 = f2
A8: Hom (a,c) <> {} by A1, A6, Th23;
 ( h * (g * f1) = (h * g) * f1 & (h * g) * f2 = h * (g * f2) ) by A1, A2, A6, Th25;
then  g * f1 = g * f2 by Defm, A4, A7, A8;
hence  f1 = f2 by Defm, A3, A6; ::_thesis: verum
end;
 Hom (b,d) <> {} by A1, A2, Th23;
hence  h * g is monic by A5, Th31; ::_thesis: verum
end;

theorem :: CAT_1:33
for C being Category
for b, c, d being Object of C
for g being Morphism of b,c
for h being Morphism of c,d st Hom (b,c) <> {} & Hom (c,d) <> {} & h * g is monic holds
g is monic
proof
let C be Category; ::_thesis: for b, c, d being Object of C
for g being Morphism of b,c
for h being Morphism of c,d st Hom (b,c) <> {} & Hom (c,d) <> {} & h * g is monic holds
g is monic
let b, c, d be Object of C; ::_thesis: for g being Morphism of b,c
for h being Morphism of c,d st Hom (b,c) <> {} & Hom (c,d) <> {} & h * g is monic holds
g is monic
let g be Morphism of b,c; ::_thesis: for h being Morphism of c,d st Hom (b,c) <> {} & Hom (c,d) <> {} & h * g is monic holds
g is monic
let h be Morphism of c,d; ::_thesis: ( Hom (b,c) <> {} & Hom (c,d) <> {} & h * g is monic implies g is monic )
assume that
A1: Hom (b,c) <> {} and
A2: Hom (c,d) <> {} and
A3: h * g is monic ; ::_thesis: g is monic
now__::_thesis:_for_a_being_Object_of_C
for_f1,_f2_being_Morphism_of_a,b_st_Hom_(a,b)_<>_{}_&_g_*_f1_=_g_*_f2_holds_
f1_=_f2
let a be Object of C; ::_thesis: for f1, f2 being Morphism of a,b st Hom (a,b) <> {} & g * f1 = g * f2 holds
f1 = f2
let f1, f2 be Morphism of a,b; ::_thesis: ( Hom (a,b) <> {} & g * f1 = g * f2 implies f1 = f2 )
A4: Hom (b,d) <> {} by A1, A2, Th23;
assume A5: Hom (a,b) <> {} ; ::_thesis: ( g * f1 = g * f2 implies f1 = f2 )
then  ( h * (g * f1) = (h * g) * f1 & h * (g * f2) = (h * g) * f2 ) by A1, A2, Th25;
hence  ( g * f1 = g * f2 implies f1 = f2 ) by A3, A5, A4, Th31; ::_thesis: verum
end;
hence  g is monic by A1, Th31; ::_thesis: verum
end;

theorem :: CAT_1:34
for C being Category
for a, b being Object of C
for h being Morphism of a,b
for g being Morphism of b,a st Hom (a,b) <> {} & Hom (b,a) <> {} & h * g = id b holds
g is monic
proof
let C be Category; ::_thesis: for a, b being Object of C
for h being Morphism of a,b
for g being Morphism of b,a st Hom (a,b) <> {} & Hom (b,a) <> {} & h * g = id b holds
g is monic
let a, b be Object of C; ::_thesis: for h being Morphism of a,b
for g being Morphism of b,a st Hom (a,b) <> {} & Hom (b,a) <> {} & h * g = id b holds
g is monic
let h be Morphism of a,b; ::_thesis: for g being Morphism of b,a st Hom (a,b) <> {} & Hom (b,a) <> {} & h * g = id b holds
g is monic
let g be Morphism of b,a; ::_thesis: ( Hom (a,b) <> {} & Hom (b,a) <> {} & h * g = id b implies g is monic )
assume that
A1: Hom (a,b) <> {} and
A2: Hom (b,a) <> {} and
A3: h * g = id b ; ::_thesis: g is monic
now__::_thesis:_for_c_being_Object_of_C
for_g1,_g2_being_Morphism_of_c,b_st_Hom_(c,b)_<>_{}_&_g_*_g1_=_g_*_g2_holds_
g1_=_g2
let c be Object of C; ::_thesis: for g1, g2 being Morphism of c,b st Hom (c,b) <> {} & g * g1 = g * g2 holds
g1 = g2
let g1, g2 be Morphism of c,b; ::_thesis: ( Hom (c,b) <> {} & g * g1 = g * g2 implies g1 = g2 )
assume that
A4: Hom (c,b) <> {} and
A5: g * g1 = g * g2 ; ::_thesis: g1 = g2
thus g1 = (h * g) * g1 by A3, A4, Th28
.= h * (g * g2) by A1, A2, A4, A5, Th25
.= (h * g) * g2 by A1, A2, A4, Th25
.= g2 by A3, A4, Th28 ; ::_thesis: verum
end;
hence  g is monic by A2, Th31; ::_thesis: verum
end;

theorem :: CAT_1:35
for C being Category
for b being Object of C holds id b is monic
proof
let C be Category; ::_thesis: for b being Object of C holds id b is monic
let b be Object of C; ::_thesis: id b is monic
A1: now__::_thesis:_for_a_being_Object_of_C
for_f1,_f2_being_Morphism_of_a,b_st_Hom_(a,b)_<>_{}_&_(id_b)_*_f1_=_(id_b)_*_f2_holds_
f1_=_f2
let a be Object of C; ::_thesis: for f1, f2 being Morphism of a,b st Hom (a,b) <> {} & (id b) * f1 = (id b) * f2 holds
f1 = f2
let f1, f2 be Morphism of a,b; ::_thesis: ( Hom (a,b) <> {} & (id b) * f1 = (id b) * f2 implies f1 = f2 )
assume A2: Hom (a,b) <> {} ; ::_thesis: ( (id b) * f1 = (id b) * f2 implies f1 = f2 )
then  (id b) * f1 = f1 by Th28;
hence  ( (id b) * f1 = (id b) * f2 implies f1 = f2 ) by A2, Th28; ::_thesis: verum
end;
 Hom (b,b) <> {} ;
hence  id b is monic by A1, Th31; ::_thesis: verum
end;

theorem Th36: :: CAT_1:36
for C being Category
for a, b being Object of C
for f being Morphism of a,b st Hom (a,b) <> {} holds
( f is epi iff for c being Object of C
for g1, g2 being Morphism of b,c st Hom (b,c) <> {} & g1 * f = g2 * f holds
g1 = g2 )
proof
let C be Category; ::_thesis: for a, b being Object of C
for f being Morphism of a,b st Hom (a,b) <> {} holds
( f is epi iff for c being Object of C
for g1, g2 being Morphism of b,c st Hom (b,c) <> {} & g1 * f = g2 * f holds
g1 = g2 )
let a, b be Object of C; ::_thesis: for f being Morphism of a,b st Hom (a,b) <> {} holds
( f is epi iff for c being Object of C
for g1, g2 being Morphism of b,c st Hom (b,c) <> {} & g1 * f = g2 * f holds
g1 = g2 )
let f be Morphism of a,b; ::_thesis: ( Hom (a,b) <> {} implies ( f is epi iff for c being Object of C
for g1, g2 being Morphism of b,c st Hom (b,c) <> {} & g1 * f = g2 * f holds
g1 = g2 ) )
assume A1: Hom (a,b) <> {} ; ::_thesis: ( f is epi iff for c being Object of C
for g1, g2 being Morphism of b,c st Hom (b,c) <> {} & g1 * f = g2 * f holds
g1 = g2 )
thus  ( f is epi implies for c being Object of C
for g1, g2 being Morphism of b,c st Hom (b,c) <> {} & g1 * f = g2 * f holds
g1 = g2 ) ::_thesis: ( ( for c being Object of C
for g1, g2 being Morphism of b,c st Hom (b,c) <> {} & g1 * f = g2 * f holds
g1 = g2 ) implies f is epi )
proof
assume that
 Hom (a,b) <> {} and
A2: for c being Object of C st Hom (b,c) <> {} holds
for g1, g2 being Morphism of b,c st g1 * f = g2 * f holds
g1 = g2 ; :: according to CAT_1:def_15 ::_thesis: for c being Object of C
for g1, g2 being Morphism of b,c st Hom (b,c) <> {} & g1 * f = g2 * f holds
g1 = g2
let c be Object of C; ::_thesis: for g1, g2 being Morphism of b,c st Hom (b,c) <> {} & g1 * f = g2 * f holds
g1 = g2
let g1, g2 be Morphism of b,c; ::_thesis: ( Hom (b,c) <> {} & g1 * f = g2 * f implies g1 = g2 )
thus  ( Hom (b,c) <> {} & g1 * f = g2 * f implies g1 = g2 ) by A2; ::_thesis: verum
end;
assume A7: for c being Object of C
for g1, g2 being Morphism of b,c st Hom (b,c) <> {} & g1 * f = g2 * f holds
g1 = g2 ; ::_thesis: f is epi
thus  Hom (a,b) <> {} by A1; :: according to CAT_1:def_15 ::_thesis: for c being Object of C st Hom (b,c) <> {} holds
for g1, g2 being Morphism of b,c st g1 * f = g2 * f holds
g1 = g2
thus  for c being Object of C st Hom (b,c) <> {} holds
for g1, g2 being Morphism of b,c st g1 * f = g2 * f holds
g1 = g2 by A7; ::_thesis: verum
end;

theorem :: CAT_1:37
for C being Category
for a, b, c being Object of C
for f being Morphism of a,b
for g being Morphism of b,c st f is epi & g is epi holds
g * f is epi
proof
let C be Category; ::_thesis: for a, b, c being Object of C
for f being Morphism of a,b
for g being Morphism of b,c st f is epi & g is epi holds
g * f is epi
let a, b, c be Object of C; ::_thesis: for f being Morphism of a,b
for g being Morphism of b,c st f is epi & g is epi holds
g * f is epi
let f be Morphism of a,b; ::_thesis: for g being Morphism of b,c st f is epi & g is epi holds
g * f is epi
let g be Morphism of b,c; ::_thesis: ( f is epi & g is epi implies g * f is epi )
assume that
A3: f is epi and
A4: g is epi ; ::_thesis: g * f is epi
A1: Hom (a,b) <> {} by A3, Defe;
A2: Hom (b,c) <> {} by A4, Defe;
A5: now__::_thesis:_for_d_being_Object_of_C
for_h1,_h2_being_Morphism_of_c,d_st_Hom_(c,d)_<>_{}_&_h1_*_(g_*_f)_=_h2_*_(g_*_f)_holds_
h1_=_h2
let d be Object of C; ::_thesis: for h1, h2 being Morphism of c,d st Hom (c,d) <> {} & h1 * (g * f) = h2 * (g * f) holds
h1 = h2
let h1, h2 be Morphism of c,d; ::_thesis: ( Hom (c,d) <> {} & h1 * (g * f) = h2 * (g * f) implies h1 = h2 )
assume that
A6: Hom (c,d) <> {} and
A7: h1 * (g * f) = h2 * (g * f) ; ::_thesis: h1 = h2
A8: Hom (b,d) <> {} by A2, A6, Th23;
 ( h1 * (g * f) = (h1 * g) * f & (h2 * g) * f = h2 * (g * f) ) by A1, A2, A6, Th25;
then  h1 * g = h2 * g by Defe, A3, A7, A8;
hence  h1 = h2 by Defe, A4, A6; ::_thesis: verum
end;
 Hom (a,c) <> {} by A1, A2, Th23;
hence  g * f is epi by A5, Th36; ::_thesis: verum
end;

theorem :: CAT_1:38
for C being Category
for a, b, c being Object of C
for f being Morphism of a,b
for g being Morphism of b,c st Hom (a,b) <> {} & Hom (b,c) <> {} & g * f is epi holds
g is epi
proof
let C be Category; ::_thesis: for a, b, c being Object of C
for f being Morphism of a,b
for g being Morphism of b,c st Hom (a,b) <> {} & Hom (b,c) <> {} & g * f is epi holds
g is epi
let a, b, c be Object of C; ::_thesis: for f being Morphism of a,b
for g being Morphism of b,c st Hom (a,b) <> {} & Hom (b,c) <> {} & g * f is epi holds
g is epi
let f be Morphism of a,b; ::_thesis: for g being Morphism of b,c st Hom (a,b) <> {} & Hom (b,c) <> {} & g * f is epi holds
g is epi
let g be Morphism of b,c; ::_thesis: ( Hom (a,b) <> {} & Hom (b,c) <> {} & g * f is epi implies g is epi )
assume that
A1: Hom (a,b) <> {} and
A2: Hom (b,c) <> {} and
A3: g * f is epi ; ::_thesis: g is epi
now__::_thesis:_for_d_being_Object_of_C
for_h1,_h2_being_Morphism_of_c,d_st_Hom_(c,d)_<>_{}_&_h1_*_g_=_h2_*_g_holds_
h1_=_h2
let d be Object of C; ::_thesis: for h1, h2 being Morphism of c,d st Hom (c,d) <> {} & h1 * g = h2 * g holds
h1 = h2
let h1, h2 be Morphism of c,d; ::_thesis: ( Hom (c,d) <> {} & h1 * g = h2 * g implies h1 = h2 )
A4: Hom (a,c) <> {} by A1, A2, Th23;
assume A5: Hom (c,d) <> {} ; ::_thesis: ( h1 * g = h2 * g implies h1 = h2 )
then  ( h1 * (g * f) = (h1 * g) * f & h2 * (g * f) = (h2 * g) * f ) by A1, A2, Th25;
hence  ( h1 * g = h2 * g implies h1 = h2 ) by A3, A5, A4, Th36; ::_thesis: verum
end;
hence  g is epi by A2, Th36; ::_thesis: verum
end;

theorem :: CAT_1:39
for C being Category
for a, b being Object of C
for h being Morphism of a,b
for g being Morphism of b,a st Hom (a,b) <> {} & Hom (b,a) <> {} & h * g = id b holds
h is epi
proof
let C be Category; ::_thesis: for a, b being Object of C
for h being Morphism of a,b
for g being Morphism of b,a st Hom (a,b) <> {} & Hom (b,a) <> {} & h * g = id b holds
h is epi
let a, b be Object of C; ::_thesis: for h being Morphism of a,b
for g being Morphism of b,a st Hom (a,b) <> {} & Hom (b,a) <> {} & h * g = id b holds
h is epi
let h be Morphism of a,b; ::_thesis: for g being Morphism of b,a st Hom (a,b) <> {} & Hom (b,a) <> {} & h * g = id b holds
h is epi
let g be Morphism of b,a; ::_thesis: ( Hom (a,b) <> {} & Hom (b,a) <> {} & h * g = id b implies h is epi )
assume that
A1: Hom (a,b) <> {} and
A2: Hom (b,a) <> {} and
A3: h * g = id b ; ::_thesis: h is epi
now__::_thesis:_for_c_being_Object_of_C
for_h1,_h2_being_Morphism_of_b,c_st_Hom_(b,c)_<>_{}_&_h1_*_h_=_h2_*_h_holds_
h1_=_h2
let c be Object of C; ::_thesis: for h1, h2 being Morphism of b,c st Hom (b,c) <> {} & h1 * h = h2 * h holds
h1 = h2
let h1, h2 be Morphism of b,c; ::_thesis: ( Hom (b,c) <> {} & h1 * h = h2 * h implies h1 = h2 )
assume that
A4: Hom (b,c) <> {} and
A5: h1 * h = h2 * h ; ::_thesis: h1 = h2
thus h1 = h1 * (h * g) by A3, A4, Th29
.= (h2 * h) * g by A1, A2, A4, A5, Th25
.= h2 * (h * g) by A1, A2, A4, Th25
.= h2 by A3, A4, Th29 ; ::_thesis: verum
end;
hence  h is epi by A1, Th36; ::_thesis: verum
end;

theorem :: CAT_1:40
for C being Category
for b being Object of C holds id b is epi
proof
let C be Category; ::_thesis: for b being Object of C holds id b is epi
let b be Object of C; ::_thesis: id b is epi
A1: now__::_thesis:_for_c_being_Object_of_C
for_g1,_g2_being_Morphism_of_b,c_st_Hom_(b,c)_<>_{}_&_g1_*_(id_b)_=_g2_*_(id_b)_holds_
g1_=_g2
let c be Object of C; ::_thesis: for g1, g2 being Morphism of b,c st Hom (b,c) <> {} & g1 * (id b) = g2 * (id b) holds
g1 = g2
let g1, g2 be Morphism of b,c; ::_thesis: ( Hom (b,c) <> {} & g1 * (id b) = g2 * (id b) implies g1 = g2 )
assume A2: Hom (b,c) <> {} ; ::_thesis: ( g1 * (id b) = g2 * (id b) implies g1 = g2 )
then  g1 * (id b) = g1 by Th29;
hence  ( g1 * (id b) = g2 * (id b) implies g1 = g2 ) by A2, Th29; ::_thesis: verum
end;
 Hom (b,b) <> {} ;
hence  id b is epi by A1, Th36; ::_thesis: verum
end;

theorem Th41: :: CAT_1:41
for C being Category
for a, b being Object of C
for f being Morphism of a,b st Hom (a,b) <> {} holds
( f is invertible iff ( Hom (b,a) <> {} & ex g being Morphism of b,a st
( f * g = id b & g * f = id a ) ) )
proof
let C be Category; ::_thesis: for a, b being Object of C
for f being Morphism of a,b st Hom (a,b) <> {} holds
( f is invertible iff ( Hom (b,a) <> {} & ex g being Morphism of b,a st
( f * g = id b & g * f = id a ) ) )
let a, b be Object of C; ::_thesis: for f being Morphism of a,b st Hom (a,b) <> {} holds
( f is invertible iff ( Hom (b,a) <> {} & ex g being Morphism of b,a st
( f * g = id b & g * f = id a ) ) )
let f be Morphism of a,b; ::_thesis: ( Hom (a,b) <> {} implies ( f is invertible iff ( Hom (b,a) <> {} & ex g being Morphism of b,a st
( f * g = id b & g * f = id a ) ) ) )
assume A1: Hom (a,b) <> {} ; ::_thesis: ( f is invertible iff ( Hom (b,a) <> {} & ex g being Morphism of b,a st
( f * g = id b & g * f = id a ) ) )
thus  ( f is invertible implies ( Hom (b,a) <> {} & ex g being Morphism of b,a st
( f * g = id b & g * f = id a ) ) ) ::_thesis: ( Hom (b,a) <> {} & ex g being Morphism of b,a st
( f * g = id b & g * f = id a ) implies f is invertible )
proof
assume A2: ( Hom (a,b) <> {} & Hom (b,a) <> {} ) ; :: according to CAT_1:def_16 ::_thesis: ( for g being Morphism of b,a holds
( not f * g = id b or not g * f = id a ) or ( Hom (b,a) <> {} & ex g being Morphism of b,a st
( f * g = id b & g * f = id a ) ) )
given g being Morphism of b,a such that A3: ( f * g = id b & g * f = id a ) ; ::_thesis: ( Hom (b,a) <> {} & ex g being Morphism of b,a st
( f * g = id b & g * f = id a ) )
thus  Hom (b,a) <> {} by A2; ::_thesis: ex g being Morphism of b,a st
( f * g = id b & g * f = id a )
take  g ; ::_thesis: ( f * g = id b & g * f = id a )
thus  ( f * g = id b & g * f = id a ) by A3; ::_thesis: verum
end;
assume A6: Hom (b,a) <> {} ; ::_thesis: ( for g being Morphism of b,a holds
( not f * g = id b or not g * f = id a ) or f is invertible )
given g being Morphism of b,a such that A7: ( f * g = id b & g * f = id a ) ; ::_thesis: f is invertible
thus  ( Hom (a,b) <> {} & Hom (b,a) <> {} ) by A1, A6; :: according to CAT_1:def_16 ::_thesis: ex g being Morphism of b,a st
( f * g = id b & g * f = id a )
take  g ; ::_thesis: ( f * g = id b & g * f = id a )
thus  ( f * g = id b & g * f = id a ) by A7; ::_thesis: verum
end;

theorem Th42: :: CAT_1:42
for C being Category
for a, b being Object of C
for f being Morphism of a,b st Hom (a,b) <> {} & Hom (b,a) <> {} holds
for g1, g2 being Morphism of b,a st f * g1 = id b & g2 * f = id a holds
g1 = g2
proof
let C be Category; ::_thesis: for a, b being Object of C
for f being Morphism of a,b st Hom (a,b) <> {} & Hom (b,a) <> {} holds
for g1, g2 being Morphism of b,a st f * g1 = id b & g2 * f = id a holds
g1 = g2
let a, b be Object of C; ::_thesis: for f being Morphism of a,b st Hom (a,b) <> {} & Hom (b,a) <> {} holds
for g1, g2 being Morphism of b,a st f * g1 = id b & g2 * f = id a holds
g1 = g2
let f be Morphism of a,b; ::_thesis: ( Hom (a,b) <> {} & Hom (b,a) <> {} implies for g1, g2 being Morphism of b,a st f * g1 = id b & g2 * f = id a holds
g1 = g2 )
assume that
A1: Hom (a,b) <> {} and
A2: Hom (b,a) <> {} ; ::_thesis: for g1, g2 being Morphism of b,a st f * g1 = id b & g2 * f = id a holds
g1 = g2
let g1, g2 be Morphism of b,a; ::_thesis: ( f * g1 = id b & g2 * f = id a implies g1 = g2 )
assume A3: f * g1 = id b ; ::_thesis: ( not g2 * f = id a or g1 = g2 )
assume  g2 * f = id a ; ::_thesis: g1 = g2
hence g1 = (g2 * f) * g1 by A2, Th28
.= g2 * (id b) by A1, A2, A3, Th25
.= g2 by A2, Th29 ;
::_thesis: verum
end;

definition
let C be Category;
let a, b be Object of C;
let f be Morphism of a,b;
assume A2: f is invertible ;
A1: Hom (a,b) <> {} by A2, Dfi;
funcf "  ->  Morphism of b,a means :Def11: :: CAT_1:def 17
( f * it = id b & it * f = id a );
existence
 ex b1 being Morphism of b,a st
( f * b1 = id b & b1 * f = id a ) by Dfi, A2;
uniqueness
 for b1, b2 being Morphism of b,a st f * b1 = id b & b1 * f = id a & f * b2 = id b & b2 * f = id a holds
b1 = b2
proof
 Hom (b,a) <> {} by Dfi, A2;
hence  for b1, b2 being Morphism of b,a st f * b1 = id b & b1 * f = id a & f * b2 = id b & b2 * f = id a holds
b1 = b2 by A1, Th42; ::_thesis: verum
end;
end;

:: deftheorem Def11 defines " CAT_1:def_17_:_
 for C being Category
for a, b being Object of C
for f being Morphism of a,b st f is invertible holds
for b5 being Morphism of b,a holds
( b5 = f " iff ( f * b5 = id b & b5 * f = id a ) );

theorem :: CAT_1:43
for C being Category
for a, b being Object of C
for f being Morphism of a,b st f is invertible holds
( f is monic & f is epi )
proof
let C be Category; ::_thesis: for a, b being Object of C
for f being Morphism of a,b st f is invertible holds
( f is monic & f is epi )
let a, b be Object of C; ::_thesis: for f being Morphism of a,b st f is invertible holds
( f is monic & f is epi )
let f be Morphism of a,b; ::_thesis: ( f is invertible implies ( f is monic & f is epi ) )
assume A2: f is invertible ; ::_thesis: ( f is monic & f is epi )
A1: Hom (a,b) <> {} by A2, Dfi;
consider k being Morphism of b,a such that
A3: f * k = id b and
A4: k * f = id a by Dfi, A2;
A5: Hom (b,a) <> {} by Dfi, A2;
now__::_thesis:_for_c_being_Object_of_C
for_g,_h_being_Morphism_of_c,a_st_Hom_(c,a)_<>_{}_&_f_*_g_=_f_*_h_holds_
g_=_h
let c be Object of C; ::_thesis: for g, h being Morphism of c,a st Hom (c,a) <> {} & f * g = f * h holds
g = h
let g, h be Morphism of c,a; ::_thesis: ( Hom (c,a) <> {} & f * g = f * h implies g = h )
assume that
A6: Hom (c,a) <> {} and
A7: f * g = f * h ; ::_thesis: g = h
g = (k * f) * g by A4, A6, Th28
.= k * (f * h) by A1, A5, A6, A7, Th25
.= (id a) * h by A1, A5, A4, A6, Th25 ;
hence  g = h by A6, Th28; ::_thesis: verum
end;
hence  f is monic by A1, Th31; ::_thesis: f is epi
now__::_thesis:_for_c_being_Object_of_C
for_g,_h_being_Morphism_of_b,c_st_Hom_(b,c)_<>_{}_&_g_*_f_=_h_*_f_holds_
g_=_h
let c be Object of C; ::_thesis: for g, h being Morphism of b,c st Hom (b,c) <> {} & g * f = h * f holds
g = h
let g, h be Morphism of b,c; ::_thesis: ( Hom (b,c) <> {} & g * f = h * f implies g = h )
assume that
A8: Hom (b,c) <> {} and
A9: g * f = h * f ; ::_thesis: g = h
g = g * (f * k) by A3, A8, Th29
.= (h * f) * k by A1, A5, A8, A9, Th25
.= h * (id b) by A1, A5, A3, A8, Th25 ;
hence  g = h by A8, Th29; ::_thesis: verum
end;
hence  f is epi by A1, Th36; ::_thesis: verum
end;

theorem :: CAT_1:44
for C being Category
for a being Object of C holds id a is invertible
proof
let C be Category; ::_thesis: for a being Object of C holds id a is invertible
let a be Object of C; ::_thesis: id a is invertible
 ( Hom (a,a) <> {} & (id a) * (id a) = id a ) ;
hence  id a is invertible by Th41; ::_thesis: verum
end;

theorem Th45: :: CAT_1:45
for C being Category
for a, b, c being Object of C
for f being Morphism of a,b
for g being Morphism of b,c st f is invertible & g is invertible holds
g * f is invertible
proof
let C be Category; ::_thesis: for a, b, c being Object of C
for f being Morphism of a,b
for g being Morphism of b,c st f is invertible & g is invertible holds
g * f is invertible
let a, b, c be Object of C; ::_thesis: for f being Morphism of a,b
for g being Morphism of b,c st f is invertible & g is invertible holds
g * f is invertible
let f be Morphism of a,b; ::_thesis: for g being Morphism of b,c st f is invertible & g is invertible holds
g * f is invertible
let g be Morphism of b,c; ::_thesis: ( f is invertible & g is invertible implies g * f is invertible )
assume A3: f is invertible ; ::_thesis: ( not g is invertible or g * f is invertible )
then A4: ( Hom (a,b) <> {} & Hom (b,a) <> {} ) by Dfi;
consider f1 being Morphism of b,a such that
A5: f * f1 = id b and
A6: f1 * f = id a by Dfi, A3;
assume A7: g is invertible ; ::_thesis: g * f is invertible
then A8: ( Hom (b,c) <> {} & Hom (c,b) <> {} ) by Dfi;
consider g1 being Morphism of c,b such that
A9: g * g1 = id c and
A10: g1 * g = id b by Dfi, A7;
A11: now__::_thesis:_(_Hom_(c,a)_<>_{}_&_ex_f1g1_being_Morphism_of_c,a_st_
(_(g_*_f)_*_f1g1_=_id_c_&_f1g1_*_(g_*_f)_=_id_a_)_)
thus A12: Hom (c,a) <> {} by A4, A8, Th23; ::_thesis: ex f1g1 being Morphism of c,a st
( (g * f) * f1g1 = id c & f1g1 * (g * f) = id a )
take f1g1 = f1 * g1; ::_thesis: ( (g * f) * f1g1 = id c & f1g1 * (g * f) = id a )
thus (g * f) * f1g1 = g * (f * (f1 * g1)) by A4, A8, A12, Th25
.= g * ((id b) * g1) by A4, A5, A8, Th25
.= id c by A8, A9, Th28 ; ::_thesis: f1g1 * (g * f) = id a
 Hom (a,c) <> {} by A4, A8, Th23;
hence f1g1 * (g * f) = f1 * (g1 * (g * f)) by A4, A8, Th25
.= f1 * ((id b) * f) by A4, A8, A10, Th25
.= id a by A4, A6, Th28 ;
::_thesis: verum
end;
 Hom (a,c) <> {} by A4, A8, Th23;
hence  g * f is invertible by A11, Th41; ::_thesis: verum
end;

theorem :: CAT_1:46
for C being Category
for a, b being Object of C
for f being Morphism of a,b st f is invertible holds
f " is invertible
proof
let C be Category; ::_thesis: for a, b being Object of C
for f being Morphism of a,b st f is invertible holds
f " is invertible
let a, b be Object of C; ::_thesis: for f being Morphism of a,b st f is invertible holds
f " is invertible
let f be Morphism of a,b; ::_thesis: ( f is invertible implies f " is invertible )
assume A2: f is invertible ; ::_thesis: f " is invertible
then A3: f * (f ") = id b by Def11;
A1: Hom (a,b) <> {} by A2, Dfi;
 ( Hom (b,a) <> {} & (f ") * f = id a ) by Dfi, A2, Def11;
hence  f " is invertible by A1, A3, Th41; ::_thesis: verum
end;

theorem :: CAT_1:47
for C being Category
for a, b, c being Object of C
for f being Morphism of a,b
for g being Morphism of b,c st f is invertible & g is invertible holds
(g * f) " = (f ") * (g ")
proof
let C be Category; ::_thesis: for a, b, c being Object of C
for f being Morphism of a,b
for g being Morphism of b,c st f is invertible & g is invertible holds
(g * f) " = (f ") * (g ")
let a, b, c be Object of C; ::_thesis: for f being Morphism of a,b
for g being Morphism of b,c st f is invertible & g is invertible holds
(g * f) " = (f ") * (g ")
let f be Morphism of a,b; ::_thesis: for g being Morphism of b,c st f is invertible & g is invertible holds
(g * f) " = (f ") * (g ")
let g be Morphism of b,c; ::_thesis: ( f is invertible & g is invertible implies (g * f) " = (f ") * (g ") )
assume that
A3: f is invertible and
A4: g is invertible ; ::_thesis: (g * f) " = (f ") * (g ")
A1: Hom (a,b) <> {} by A3, Dfi;
A2: Hom (b,c) <> {} by A4, Dfi;
A5: Hom (c,b) <> {} by Dfi, A4;
A6: Hom (b,a) <> {} by Dfi, A3;
then A7: Hom (c,a) <> {} by A5, Th23;
then A8: ((f ") * (g ")) * (g * f) = (((f ") * (g ")) * g) * f by A1, A2, Th25
.= ((f ") * ((g ") * g)) * f by A2, A6, A5, Th25
.= ((f ") * (id b)) * f by A4, Def11
.= (f ") * f by A6, Th29
.= id a by A3, Def11 ;
A9: ( Hom (a,c) <> {} & g * f is invertible ) by A1, A2, A3, A4, Th23, Th45;
(g * f) * ((f ") * (g ")) = g * (f * ((f ") * (g "))) by A1, A2, A7, Th25
.= g * ((f * (f ")) * (g ")) by A1, A6, A5, Th25
.= g * ((id b) * (g ")) by A3, Def11
.= g * (g ") by A5, Th28
.= id c by A4, Def11 ;
hence  (g * f) " = (f ") * (g ") by A8, A9, Def11; ::_thesis: verum
end;

definition
let C be Category;
let a be Object of C;
attra is terminal  means :Def12: :: CAT_1:def 18
 for b being Object of C holds
( Hom (b,a) <> {} & ex f being Morphism of b,a st
for g being Morphism of b,a holds f = g );
attra is initial  means :Def13: :: CAT_1:def 19
 for b being Object of C holds
( Hom (a,b) <> {} & ex f being Morphism of a,b st
for g being Morphism of a,b holds f = g );
let b be Object of C;
preda,b are_isomorphic  means :: CAT_1:def 20
 ex f being Morphism of a,b st f is invertible ;
reflexivity
 for a being Object of C ex f being Morphism of a,a st f is invertible
proof
let a be Object of C; ::_thesis: ex f being Morphism of a,a st f is invertible
A1: Hom (a,a) <> {} ;
take  id a ; ::_thesis: id a is invertible
 (id a) * (id a) = id a ;
hence  id a is invertible by A1, Th41; ::_thesis: verum
end;
symmetry
 for a, b being Object of C st ex f being Morphism of a,b st f is invertible holds
ex f being Morphism of b,a st f is invertible
proof
let a, b be Object of C; ::_thesis: ( ex f being Morphism of a,b st f is invertible implies ex f being Morphism of b,a st f is invertible )
given f being Morphism of a,b such that A2: f is invertible ; ::_thesis: ex f being Morphism of b,a st f is invertible
A3: ( Hom (b,a) <> {} & Hom (a,b) <> {} ) by A2, Dfi;
consider g being Morphism of b,a such that
A4: ( f * g = id b & g * f = id a ) by A2, Dfi;
take  g ; ::_thesis: g is invertible
thus  g is invertible by A3, A4, Dfi; ::_thesis: verum
end;
end;

:: deftheorem Def12 defines terminal CAT_1:def_18_:_
 for C being Category
for a being Object of C holds
( a is terminal iff for b being Object of C holds
( Hom (b,a) <> {} & ex f being Morphism of b,a st
for g being Morphism of b,a holds f = g ) );

:: deftheorem Def13 defines initial CAT_1:def_19_:_
 for C being Category
for a being Object of C holds
( a is initial iff for b being Object of C holds
( Hom (a,b) <> {} & ex f being Morphism of a,b st
for g being Morphism of a,b holds f = g ) );

:: deftheorem  defines are_isomorphic CAT_1:def_20_:_
 for C being Category
for a, b being Object of C holds
( a,b are_isomorphic iff ex f being Morphism of a,b st f is invertible );

theorem :: CAT_1:48
for C being Category
for a, b being Object of C holds
( a,b are_isomorphic iff ( Hom (a,b) <> {} & Hom (b,a) <> {} & ex f being Morphism of a,b ex f9 being Morphism of b,a st
( f * f9 = id b & f9 * f = id a ) ) )
proof
let C be Category; ::_thesis: for a, b being Object of C holds
( a,b are_isomorphic iff ( Hom (a,b) <> {} & Hom (b,a) <> {} & ex f being Morphism of a,b ex f9 being Morphism of b,a st
( f * f9 = id b & f9 * f = id a ) ) )
let a, b be Object of C; ::_thesis: ( a,b are_isomorphic iff ( Hom (a,b) <> {} & Hom (b,a) <> {} & ex f being Morphism of a,b ex f9 being Morphism of b,a st
( f * f9 = id b & f9 * f = id a ) ) )
thus  ( a,b are_isomorphic implies ( Hom (a,b) <> {} & Hom (b,a) <> {} & ex f being Morphism of a,b ex f9 being Morphism of b,a st
( f * f9 = id b & f9 * f = id a ) ) ) ::_thesis: ( Hom (a,b) <> {} & Hom (b,a) <> {} & ex f being Morphism of a,b ex f9 being Morphism of b,a st
( f * f9 = id b & f9 * f = id a ) implies a,b are_isomorphic )
proof
given f being Morphism of a,b such that A2: f is invertible ; :: according to CAT_1:def_20 ::_thesis: ( Hom (a,b) <> {} & Hom (b,a) <> {} & ex f being Morphism of a,b ex f9 being Morphism of b,a st
( f * f9 = id b & f9 * f = id a ) )
thus  ( Hom (a,b) <> {} & Hom (b,a) <> {} ) by A2, Dfi; ::_thesis: ex f being Morphism of a,b ex f9 being Morphism of b,a st
( f * f9 = id b & f9 * f = id a )
take  f ; ::_thesis: ex f9 being Morphism of b,a st
( f * f9 = id b & f9 * f = id a )
thus  ex f9 being Morphism of b,a st
( f * f9 = id b & f9 * f = id a ) by A2, Dfi; ::_thesis: verum
end;
assume that
A3: Hom (a,b) <> {} and
A4: Hom (b,a) <> {} ; ::_thesis: ( for f being Morphism of a,b
for f9 being Morphism of b,a holds
( not f * f9 = id b or not f9 * f = id a ) or a,b are_isomorphic )
given f being Morphism of a,b such that A5: ex f9 being Morphism of b,a st
( f * f9 = id b & f9 * f = id a ) ; ::_thesis: a,b are_isomorphic
take  f ; :: according to CAT_1:def_20 ::_thesis: f is invertible
thus  f is invertible by A3, A4, A5, Th41; ::_thesis: verum
end;

theorem :: CAT_1:49
for C being Category
for a being Object of C holds
( a is initial iff for b being Object of C ex f being Morphism of a,b st Hom (a,b) = {f} )
proof
let C be Category; ::_thesis: for a being Object of C holds
( a is initial iff for b being Object of C ex f being Morphism of a,b st Hom (a,b) = {f} )
let a be Object of C; ::_thesis: ( a is initial iff for b being Object of C ex f being Morphism of a,b st Hom (a,b) = {f} )
thus  ( a is initial implies for b being Object of C ex f being Morphism of a,b st Hom (a,b) = {f} ) ::_thesis: ( ( for b being Object of C ex f being Morphism of a,b st Hom (a,b) = {f} ) implies a is initial )
proof
assume A1: a is initial ; ::_thesis: for b being Object of C ex f being Morphism of a,b st Hom (a,b) = {f}
let b be Object of C; ::_thesis: ex f being Morphism of a,b st Hom (a,b) = {f}
consider f being Morphism of a,b such that
A2: for g being Morphism of a,b holds f = g by A1, Def13;
take  f ; ::_thesis: Hom (a,b) = {f}
thus  Hom (a,b) = {f} by A2, Th8, A1, Def13; ::_thesis: verum
end;
assume A3: for b being Object of C ex f being Morphism of a,b st Hom (a,b) = {f} ; ::_thesis: a is initial
let b be Object of C; :: according to CAT_1:def_19 ::_thesis: ( Hom (a,b) <> {} & ex f being Morphism of a,b st
for g being Morphism of a,b holds f = g )
consider f being Morphism of a,b such that
A4: Hom (a,b) = {f} by A3;
thus  Hom (a,b) <> {} by A4; ::_thesis: ex f being Morphism of a,b st
for g being Morphism of a,b holds f = g
take  f ; ::_thesis: for g being Morphism of a,b holds f = g
thus  for g being Morphism of a,b holds f = g by A4, Th7; ::_thesis: verum
end;

theorem Th50: :: CAT_1:50
for C being Category
for a being Object of C st a is initial holds
for h being Morphism of a,a holds id a = h
proof
let C be Category; ::_thesis: for a being Object of C st a is initial holds
for h being Morphism of a,a holds id a = h
let a be Object of C; ::_thesis: ( a is initial implies for h being Morphism of a,a holds id a = h )
assume  a is initial ; ::_thesis: for h being Morphism of a,a holds id a = h
then consider f being Morphism of a,a such that
A1: for g being Morphism of a,a holds f = g by Def13;
let h be Morphism of a,a; ::_thesis: id a = h
 id a = f by A1;
hence  id a = h by A1; ::_thesis: verum
end;

theorem :: CAT_1:51
for C being Category
for a, b being Object of C st a is initial & b is initial holds
a,b are_isomorphic
proof
let C be Category; ::_thesis: for a, b being Object of C st a is initial & b is initial holds
a,b are_isomorphic
let a, b be Object of C; ::_thesis: ( a is initial & b is initial implies a,b are_isomorphic )
assume that
A1: a is initial and
A2: b is initial ; ::_thesis: a,b are_isomorphic
set g = the Morphism of b,a;
set f = the Morphism of a,b;
A3: Hom (a,b) <> {} by A1, Def13;
take  the Morphism of a,b ; :: according to CAT_1:def_20 ::_thesis: the Morphism of a,b is invertible
now__::_thesis:_(_Hom_(b,a)_<>_{}_&_ex_g_being_Morphism_of_b,a_st_
(_the_Morphism_of_a,b_*_g_=_id_b_&_g_*_the_Morphism_of_a,b_=_id_a_)_)
thus  Hom (b,a) <> {} by A2, Def13; ::_thesis: ex g being Morphism of b,a st
( the Morphism of a,b * g = id b & g * the Morphism of a,b = id a )
take g = the Morphism of b,a; ::_thesis: ( the Morphism of a,b * g = id b & g * the Morphism of a,b = id a )
thus  ( the Morphism of a,b * g = id b & g * the Morphism of a,b = id a ) by A1, A2, Th50; ::_thesis: verum
end;
hence  the Morphism of a,b is invertible by A3, Th41; ::_thesis: verum
end;

theorem :: CAT_1:52
for C being Category
for a, b being Object of C st a is initial & a,b are_isomorphic holds
b is initial
proof
let C be Category; ::_thesis: for a, b being Object of C st a is initial & a,b are_isomorphic holds
b is initial
let a, b be Object of C; ::_thesis: ( a is initial & a,b are_isomorphic implies b is initial )
assume A1: a is initial ; ::_thesis: ( not a,b are_isomorphic or b is initial )
given f being Morphism of a,b such that A2: f is invertible ; :: according to CAT_1:def_20 ::_thesis: b is initial
A3: Hom (b,a) <> {} by A2, Dfi;
let c be Object of C; :: according to CAT_1:def_19 ::_thesis: ( Hom (b,c) <> {} & ex f being Morphism of b,c st
for g being Morphism of b,c holds f = g )
consider h being Morphism of a,c such that
A4: for g being Morphism of a,c holds h = g by A1, Def13;
 Hom (a,c) <> {} by A1, Def13;
hence A5: Hom (b,c) <> {} by A3, Th23; ::_thesis: ex f being Morphism of b,c st
for g being Morphism of b,c holds f = g
consider f9 being Morphism of b,a such that
A6: f * f9 = id b and
 f9 * f = id a by A2, Dfi;
A7: Hom (a,b) <> {} by A2, Dfi;
take  h * f9 ; ::_thesis: for g being Morphism of b,c holds h * f9 = g
let h9 be Morphism of b,c; ::_thesis: h * f9 = h9
thus h9 = h9 * (f * f9) by A6, A5, Th29
.= (h9 * f) * f9 by A3, A5, A7, Th25
.= h * f9 by A4 ; ::_thesis: verum
end;

theorem :: CAT_1:53
for C being Category
for b being Object of C holds
( b is terminal iff for a being Object of C ex f being Morphism of a,b st Hom (a,b) = {f} )
proof
let C be Category; ::_thesis: for b being Object of C holds
( b is terminal iff for a being Object of C ex f being Morphism of a,b st Hom (a,b) = {f} )
let b be Object of C; ::_thesis: ( b is terminal iff for a being Object of C ex f being Morphism of a,b st Hom (a,b) = {f} )
thus  ( b is terminal implies for a being Object of C ex f being Morphism of a,b st Hom (a,b) = {f} ) ::_thesis: ( ( for a being Object of C ex f being Morphism of a,b st Hom (a,b) = {f} ) implies b is terminal )
proof
assume A1: b is terminal ; ::_thesis: for a being Object of C ex f being Morphism of a,b st Hom (a,b) = {f}
let a be Object of C; ::_thesis: ex f being Morphism of a,b st Hom (a,b) = {f}
consider f being Morphism of a,b such that
A2: for g being Morphism of a,b holds f = g by A1, Def12;
take  f ; ::_thesis: Hom (a,b) = {f}
thus  Hom (a,b) = {f} by A2, Th8, A1, Def12; ::_thesis: verum
end;
assume A3: for a being Object of C ex f being Morphism of a,b st Hom (a,b) = {f} ; ::_thesis: b is terminal
let a be Object of C; :: according to CAT_1:def_18 ::_thesis: ( Hom (a,b) <> {} & ex f being Morphism of a,b st
for g being Morphism of a,b holds f = g )
consider f being Morphism of a,b such that
A4: Hom (a,b) = {f} by A3;
thus  Hom (a,b) <> {} by A4; ::_thesis: ex f being Morphism of a,b st
for g being Morphism of a,b holds f = g
take  f ; ::_thesis: for g being Morphism of a,b holds f = g
thus  for g being Morphism of a,b holds f = g by A4, Th7; ::_thesis: verum
end;

theorem Th54: :: CAT_1:54
for C being Category
for a being Object of C st a is terminal holds
for h being Morphism of a,a holds id a = h
proof
let C be Category; ::_thesis: for a being Object of C st a is terminal holds
for h being Morphism of a,a holds id a = h
let a be Object of C; ::_thesis: ( a is terminal implies for h being Morphism of a,a holds id a = h )
assume  a is terminal ; ::_thesis: for h being Morphism of a,a holds id a = h
then consider f being Morphism of a,a such that
A1: for g being Morphism of a,a holds f = g by Def12;
let h be Morphism of a,a; ::_thesis: id a = h
 id a = f by A1;
hence  id a = h by A1; ::_thesis: verum
end;

theorem :: CAT_1:55
for C being Category
for a, b being Object of C st a is terminal & b is terminal holds
a,b are_isomorphic
proof
let C be Category; ::_thesis: for a, b being Object of C st a is terminal & b is terminal holds
a,b are_isomorphic
let a, b be Object of C; ::_thesis: ( a is terminal & b is terminal implies a,b are_isomorphic )
assume that
A1: a is terminal and
A2: b is terminal ; ::_thesis: a,b are_isomorphic
set g = the Morphism of b,a;
set f = the Morphism of a,b;
A3: Hom (a,b) <> {} by A2, Def12;
take  the Morphism of a,b ; :: according to CAT_1:def_20 ::_thesis: the Morphism of a,b is invertible
now__::_thesis:_(_Hom_(b,a)_<>_{}_&_ex_g_being_Morphism_of_b,a_st_
(_the_Morphism_of_a,b_*_g_=_id_b_&_g_*_the_Morphism_of_a,b_=_id_a_)_)
thus  Hom (b,a) <> {} by A1, Def12; ::_thesis: ex g being Morphism of b,a st
( the Morphism of a,b * g = id b & g * the Morphism of a,b = id a )
take g = the Morphism of b,a; ::_thesis: ( the Morphism of a,b * g = id b & g * the Morphism of a,b = id a )
thus  ( the Morphism of a,b * g = id b & g * the Morphism of a,b = id a ) by A1, A2, Th54; ::_thesis: verum
end;
hence  the Morphism of a,b is invertible by A3, Th41; ::_thesis: verum
end;

theorem :: CAT_1:56
for C being Category
for b, a being Object of C st b is terminal & a,b are_isomorphic holds
a is terminal
proof
let C be Category; ::_thesis: for b, a being Object of C st b is terminal & a,b are_isomorphic holds
a is terminal
let b, a be Object of C; ::_thesis: ( b is terminal & a,b are_isomorphic implies a is terminal )
assume A1: b is terminal ; ::_thesis: ( not a,b are_isomorphic or a is terminal )
given f being Morphism of a,b such that A2: f is invertible ; :: according to CAT_1:def_20 ::_thesis: a is terminal
A3: Hom (b,a) <> {} by A2, Dfi;
let c be Object of C; :: according to CAT_1:def_18 ::_thesis: ( Hom (c,a) <> {} & ex f being Morphism of c,a st
for g being Morphism of c,a holds f = g )
consider h being Morphism of c,b such that
A4: for g being Morphism of c,b holds h = g by A1, Def12;
 Hom (c,b) <> {} by A1, Def12;
hence A5: Hom (c,a) <> {} by A3, Th23; ::_thesis: ex f being Morphism of c,a st
for g being Morphism of c,a holds f = g
consider f9 being Morphism of b,a such that
 f * f9 = id b and
A6: f9 * f = id a by A2, Dfi;
A7: Hom (a,b) <> {} by A2, Dfi;
take  f9 * h ; ::_thesis: for g being Morphism of c,a holds f9 * h = g
let h9 be Morphism of c,a; ::_thesis: f9 * h = h9
thus f9 * h = f9 * (f * h9) by A4
.= (f9 * f) * h9 by A3, A5, A7, Th25
.= h9 by A6, A5, Th28 ; ::_thesis: verum
end;

theorem :: CAT_1:57
for C being Category
for a, b being Object of C
for f being Morphism of a,b st Hom (a,b) <> {} & a is terminal holds
f is monic
proof
let C be Category; ::_thesis: for a, b being Object of C
for f being Morphism of a,b st Hom (a,b) <> {} & a is terminal holds
f is monic
let a, b be Object of C; ::_thesis: for f being Morphism of a,b st Hom (a,b) <> {} & a is terminal holds
f is monic
let f be Morphism of a,b; ::_thesis: ( Hom (a,b) <> {} & a is terminal implies f is monic )
assume that
A1: Hom (a,b) <> {} and
A2: a is terminal ; ::_thesis: f is monic
now__::_thesis:_for_c_being_Object_of_C
for_g,_h_being_Morphism_of_c,a_st_Hom_(c,a)_<>_{}_&_f_*_g_=_f_*_h_holds_
g_=_h
let c be Object of C; ::_thesis: for g, h being Morphism of c,a st Hom (c,a) <> {} & f * g = f * h holds
g = h
let g, h be Morphism of c,a; ::_thesis: ( Hom (c,a) <> {} & f * g = f * h implies g = h )
assume that
 Hom (c,a) <> {} and
 f * g = f * h ; ::_thesis: g = h
consider ff being Morphism of c,a such that
A3: for gg being Morphism of c,a holds ff = gg by A2, Def12;
 ff = g by A3;
hence  g = h by A3; ::_thesis: verum
end;
hence  f is monic by A1, Th31; ::_thesis: verum
end;

registration
let C be Category;
let a be Object of C;
reduce dom (id a) to a;
reducibility
 dom (id a) = a
proof
 id a in Hom (a,a) by Def4;
hence  dom (id a) = a by Th1; ::_thesis: verum
end;
reduce cod (id a) to a;
reducibility
 cod (id a) = a
proof
 id a in Hom (a,a) by Def4;
hence  cod (id a) = a by Th1; ::_thesis: verum
end;
end;

theorem Th58: :: CAT_1:58
for C being Category
for a being Object of C holds
( dom (id a) = a & cod (id a) = a ) ;

theorem Th59: :: CAT_1:59
for C being Category
for a, b being Object of C st id a = id b holds
a = b
proof
let C be Category; ::_thesis: for a, b being Object of C st id a = id b holds
a = b
let a, b be Object of C; ::_thesis: ( id a = id b implies a = b )
assume Z: id a = id b ; ::_thesis: a = b
thus a = dom (id a)
.= b by Th58, Z ; ::_thesis: verum
end;

theorem :: CAT_1:60
for C being Category
for a, b, c being Object of C st a,b are_isomorphic & b,c are_isomorphic holds
a,c are_isomorphic
proof
let C be Category; ::_thesis: for a, b, c being Object of C st a,b are_isomorphic & b,c are_isomorphic holds
a,c are_isomorphic
let a, b, c be Object of C; ::_thesis: ( a,b are_isomorphic & b,c are_isomorphic implies a,c are_isomorphic )
given f being Morphism of a,b such that A2: f is invertible ; :: according to CAT_1:def_20 ::_thesis: ( not b,c are_isomorphic or a,c are_isomorphic )
given g being Morphism of b,c such that A4: g is invertible ; :: according to CAT_1:def_20 ::_thesis: a,c are_isomorphic
take  g * f ; :: according to CAT_1:def_20 ::_thesis: g * f is invertible
thus  g * f is invertible by A2, A4, Th45; ::_thesis: verum
end;

definition
let C, D be Category;
mode Functor of C,D ->  Function of the carrier' of C, the carrier' of D means :Def15: :: CAT_1:def 21
( ( for c being Element of C ex d being Element of D st it . (id c) = id d ) & ( for f being Element of the carrier' of C holds
( it . (id (dom f)) = id (dom (it . f)) & it . (id (cod f)) = id (cod (it . f)) ) ) & ( for f, g being Element of the carrier' of C st [g,f] in dom the Comp of C holds
it . (g (*) f) = (it . g) (*) (it . f) ) );
existence
 ex b1 being Function of the carrier' of C, the carrier' of D st
( ( for c being Element of C ex d being Element of D st b1 . (id c) = id d ) & ( for f being Element of the carrier' of C holds
( b1 . (id (dom f)) = id (dom (b1 . f)) & b1 . (id (cod f)) = id (cod (b1 . f)) ) ) & ( for f, g being Element of the carrier' of C st [g,f] in dom the Comp of C holds
b1 . (g (*) f) = (b1 . g) (*) (b1 . f) ) )
proof
set d = the Element of D;
reconsider F = the carrier' of C --> (id the Element of D) as Function of the carrier' of C, the carrier' of D ;
take  F ; ::_thesis: ( ( for c being Element of C ex d being Element of D st F . (id c) = id d ) & ( for f being Element of the carrier' of C holds
( F . (id (dom f)) = id (dom (F . f)) & F . (id (cod f)) = id (cod (F . f)) ) ) & ( for f, g being Element of the carrier' of C st [g,f] in dom the Comp of C holds
F . (g (*) f) = (F . g) (*) (F . f) ) )
thus  for c being Element of C ex d being Element of D st F . (id c) = id d by FUNCOP_1:7; ::_thesis: ( ( for f being Element of the carrier' of C holds
( F . (id (dom f)) = id (dom (F . f)) & F . (id (cod f)) = id (cod (F . f)) ) ) & ( for f, g being Element of the carrier' of C st [g,f] in dom the Comp of C holds
F . (g (*) f) = (F . g) (*) (F . f) ) )
A1: Hom ( the Element of D, the Element of D) <> {} ;
thus  for f being Element of the carrier' of C holds
( F . (id (dom f)) = id (dom (F . f)) & F . (id (cod f)) = id (cod (F . f)) ) ::_thesis: for f, g being Element of the carrier' of C st [g,f] in dom the Comp of C holds
F . (g (*) f) = (F . g) (*) (F . f)
proof
let f be Element of the carrier' of C; ::_thesis: ( F . (id (dom f)) = id (dom (F . f)) & F . (id (cod f)) = id (cod (F . f)) )
A2: F . f = id the Element of D by FUNCOP_1:7;
thus F . (id (dom f)) = id the Element of D by FUNCOP_1:7
.= id (dom (F . f)) by A2, Th58 ; ::_thesis: F . (id (cod f)) = id (cod (F . f))
thus F . (id (cod f)) = id the Element of D by FUNCOP_1:7
.= id (cod (F . f)) by A2, Th58 ; ::_thesis: verum
end;
let f, g be Element of the carrier' of C; ::_thesis: ( [g,f] in dom the Comp of C implies F . (g (*) f) = (F . g) (*) (F . f) )
assume  [g,f] in dom the Comp of C ; ::_thesis: F . (g (*) f) = (F . g) (*) (F . f)
thus F . (g (*) f) = (id the Element of D) * (id the Element of D) by FUNCOP_1:7
.= (id the Element of D) (*) (id the Element of D) by A1, Def10
.= (id the Element of D) (*) (F . f) by FUNCOP_1:7
.= (F . g) (*) (F . f) by FUNCOP_1:7 ; ::_thesis: verum
end;
end;

:: deftheorem Def15 defines Functor CAT_1:def_21_:_
 for C, D being Category
for b3 being Function of the carrier' of C, the carrier' of D holds
( b3 is Functor of C,D iff ( ( for c being Element of C ex d being Element of D st b3 . (id c) = id d ) & ( for f being Element of the carrier' of C holds
( b3 . (id (dom f)) = id (dom (b3 . f)) & b3 . (id (cod f)) = id (cod (b3 . f)) ) ) & ( for f, g being Element of the carrier' of C st [g,f] in dom the Comp of C holds
b3 . (g (*) f) = (b3 . g) (*) (b3 . f) ) ) );

theorem Th61: :: CAT_1:61
for C, D being Category
for T being Function of the carrier' of C, the carrier' of D st ( 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) ) holds
T is Functor of C,D
proof
let C, D be Category; ::_thesis: for T being Function of the carrier' of C, the carrier' of D st ( 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) ) holds
T is Functor of C,D
let T be Function of the carrier' of C, the carrier' of D; ::_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) ) implies T is Functor of C,D )
assume that
A1: for c being Object of C ex d being Object of D st T . (id c) = id d and
A2: for f being Morphism of C holds
( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) ) and
A3: for f, g being Morphism of C st dom g = cod f holds
T . (g (*) f) = (T . g) (*) (T . f) ; ::_thesis: T is Functor of C,D
thus  for c being Element of C ex d being Element of D st T . (id c) = id d by A1; :: according to CAT_1:def_21 ::_thesis: ( ( for f being Element of the carrier' of C holds
( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) ) ) & ( for f, g being Element of the carrier' of C st [g,f] in dom the Comp of C holds
T . (g (*) f) = (T . g) (*) (T . f) ) )
thus  for f being Element of the carrier' of C holds
( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) ) by A2; ::_thesis: for f, g being Element of the carrier' of C st [g,f] in dom the Comp of C holds
T . (g (*) f) = (T . g) (*) (T . f)
let f, g be Element of the carrier' of C; ::_thesis: ( [g,f] in dom the Comp of C implies T . (g (*) f) = (T . g) (*) (T . f) )
assume  [g,f] in dom the Comp of C ; ::_thesis: T . (g (*) f) = (T . g) (*) (T . f)
then A5: dom g = cod f by Def5a;
thus  T . (g (*) f) = (T . g) (*) (T . f) by A3, A5; ::_thesis: verum
end;

theorem :: CAT_1:62
for C, D being Category
for T being Functor of C,D
for c being Object of C ex d being Object of D st T . (id c) = id d by Def15;

theorem :: CAT_1:63
for C, D being Category
for T being Functor of C,D
for f being Morphism of C holds
( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) ) by Def15;

theorem Th64: :: CAT_1:64
for C, D being Category
for T being Functor of C,D
for f, g being Morphism of C st dom g = cod f holds
( dom (T . g) = cod (T . f) & T . (g (*) f) = (T . g) (*) (T . f) )
proof
let C, D be Category; ::_thesis: for T being Functor of C,D
for f, g being Morphism of C st dom g = cod f holds
( dom (T . g) = cod (T . f) & T . (g (*) f) = (T . g) (*) (T . f) )
let T be Functor of C,D; ::_thesis: for f, g being Morphism of C st dom g = cod f holds
( dom (T . g) = cod (T . f) & T . (g (*) f) = (T . g) (*) (T . f) )
let f, g be Morphism of C; ::_thesis: ( dom g = cod f implies ( dom (T . g) = cod (T . f) & T . (g (*) f) = (T . g) (*) (T . f) ) )
assume A1: dom g = cod f ; ::_thesis: ( dom (T . g) = cod (T . f) & T . (g (*) f) = (T . g) (*) (T . f) )
then A2: ( the Comp of C . (g,f) = g (*) f & [g,f] in dom the Comp of C ) by Def5a, Th16;
id (dom (T . g)) = T . (id (cod f)) by A1, Def15
.= id (cod (T . f)) by Def15 ;
hence  dom (T . g) = cod (T . f) by Th59; ::_thesis: T . (g (*) f) = (T . g) (*) (T . f)
thus  T . (g (*) f) = (T . g) (*) (T . f) by A2, Def15; ::_thesis: verum
end;

theorem Th65: :: CAT_1:65
for C, D being Category
for T being Function of the carrier' of C, the carrier' of D
for F being Function of the carrier of C, the carrier of D st ( for c being Object of C holds T . (id c) = id (F . c) ) & ( for f being Morphism of C holds
( F . (dom f) = dom (T . f) & F . (cod f) = cod (T . f) ) ) & ( for f, g being Morphism of C st dom g = cod f holds
T . (g (*) f) = (T . g) (*) (T . f) ) holds
T is Functor of C,D
proof
let C, D be Category; ::_thesis: for T being Function of the carrier' of C, the carrier' of D
for F being Function of the carrier of C, the carrier of D st ( for c being Object of C holds T . (id c) = id (F . c) ) & ( for f being Morphism of C holds
( F . (dom f) = dom (T . f) & F . (cod f) = cod (T . f) ) ) & ( for f, g being Morphism of C st dom g = cod f holds
T . (g (*) f) = (T . g) (*) (T . f) ) holds
T is Functor of C,D
let T be Function of the carrier' of C, the carrier' of D; ::_thesis: for F being Function of the carrier of C, the carrier of D st ( for c being Object of C holds T . (id c) = id (F . c) ) & ( for f being Morphism of C holds
( F . (dom f) = dom (T . f) & F . (cod f) = cod (T . f) ) ) & ( for f, g being Morphism of C st dom g = cod f holds
T . (g (*) f) = (T . g) (*) (T . f) ) holds
T is Functor of C,D
let F be Function of the carrier of C, the carrier of D; ::_thesis: ( ( for c being Object of C holds T . (id c) = id (F . c) ) & ( for f being Morphism of C holds
( F . (dom f) = dom (T . f) & F . (cod f) = cod (T . f) ) ) & ( for f, g being Morphism of C st dom g = cod f holds
T . (g (*) f) = (T . g) (*) (T . f) ) implies T is Functor of C,D )
assume that
A1: for c being Object of C holds T . (id c) = id (F . c) and
A2: for f being Morphism of C holds
( F . (dom f) = dom (T . f) & F . (cod f) = cod (T . f) ) and
A3: for f, g being Morphism of C st dom g = cod f holds
T . (g (*) f) = (T . g) (*) (T . f) ; ::_thesis: T is Functor of C,D
A4: for c being Object of C ex d being Object of D st T . (id c) = id d
proof
let c be Object of C; ::_thesis: ex d being Object of D st T . (id c) = id d
take  F . c ; ::_thesis: T . (id c) = id (F . c)
thus  T . (id c) = id (F . c) by A1; ::_thesis: verum
end;
 for f being Morphism of C holds
( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (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)) = id (F . (dom f)) by A1
.= id (dom (T . f)) by A2 ; ::_thesis: T . (id (cod f)) = id (cod (T . f))
thus T . (id (cod f)) = id (F . (cod f)) by A1
.= id (cod (T . f)) by A2 ; ::_thesis: verum
end;
hence  T is Functor of C,D by A3, A4, Th61; ::_thesis: verum
end;

definition
let C, D be Category;
let F be Function of the carrier' of C, the carrier' of D;
assume A1: for c being Element of C ex d being Element of D st F . (id c) = id d ;
func Obj F ->  Function of the carrier of C, the carrier of D means :Def16: :: CAT_1:def 22
 for c being Element of C
for d being Element of D st F . (id c) = id d holds
it . c = d;
existence
 ex b1 being Function of the carrier of C, the carrier of D st
for c being Element of C
for d being Element of D st F . (id c) = id d holds
b1 . c = d
proof
defpred S1[ Object of C, Object of D] means  for d being Element of D st F . (id $1) = id d holds
$2 = d;
A2: for c being Element of C ex y being Element of D st S1[c,y]
proof
let c be Element of C; ::_thesis: ex y being Element of D st S1[c,y]
consider y being Element of D such that
A3: F . (id c) = id y by A1;
take  y ; ::_thesis: S1[c,y]
let d be Element of D; ::_thesis: ( F . (id c) = id d implies y = d )
assume  F . (id c) = id d ; ::_thesis: y = d
hence  y = d by A3, Th59; ::_thesis: verum
end;
thus  ex f being Function of the carrier of C, the carrier of D st
for x being Element of C holds S1[x,f . x] from FUNCT_2:sch_3(A2); ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of the carrier of C, the carrier of D st ( for c being Element of C
for d being Element of D st F . (id c) = id d holds
b1 . c = d ) & ( for c being Element of C
for d being Element of D st F . (id c) = id d holds
b2 . c = d ) holds
b1 = b2
proof
let F1, F2 be Function of the carrier of C, the carrier of D; ::_thesis: ( ( for c being Element of C
for d being Element of D st F . (id c) = id d holds
F1 . c = d ) & ( for c being Element of C
for d being Element of D st F . (id c) = id d holds
F2 . c = d ) implies F1 = F2 )
assume that
A5: for c being Element of C
for d being Element of D st F . (id c) = id d holds
F1 . c = d and
A6: for c being Element of C
for d being Element of D st F . (id c) = id d holds
F2 . c = d ; ::_thesis: F1 = F2
 for c being Element of C holds F1 . c = F2 . c
proof
let c be Element of C; ::_thesis: F1 . c = F2 . c
consider d1 being Element of D such that
A7: F . (id c) = id d1 by A1;
 F1 . c = d1 by A5, A7;
hence  F1 . c = F2 . c by A6, A7; ::_thesis: verum
end;
hence  F1 = F2 by FUNCT_2:63; ::_thesis: verum
end;
end;

:: deftheorem Def16 defines Obj CAT_1:def_22_:_
 for C, D being Category
for F being Function of the carrier' of C, the carrier' of D st ( for c being Element of C ex d being Element of D st F . (id c) = id d ) holds
for b4 being Function of the carrier of C, the carrier of D holds
( b4 = Obj F iff for c being Element of C
for d being Element of D st F . (id c) = id d holds
b4 . c = d );

theorem :: CAT_1:66
for C, D being Category
for T being Function of the carrier' of C, the carrier' of D st ( for c being Object of C ex d being Object of D st T . (id c) = id d ) holds
for c being Object of C
for d being Object of D st T . (id c) = id d holds
(Obj T) . c = d by Def16;

theorem Th67: :: CAT_1:67
for C, D being Category
for T being Functor of C,D
for c being Object of C
for d being Object of D st T . (id c) = id d holds
(Obj T) . c = d
proof
let C, D be Category; ::_thesis: for T being Functor of C,D
for c being Object of C
for d being Object of D st T . (id c) = id d holds
(Obj T) . c = d
let T be Functor of C,D; ::_thesis: for c being Object of C
for d being Object of D st T . (id c) = id d holds
(Obj T) . c = d
 for c being Object of C ex d being Object of D st T . (id c) = id d by Def15;
hence  for c being Object of C
for d being Object of D st T . (id c) = id d holds
(Obj T) . c = d by Def16; ::_thesis: verum
end;

theorem Th68: :: CAT_1:68
for C, D being Category
for T being Functor of C,D
for c being Object of C holds T . (id c) = id ((Obj T) . c)
proof
let C, D be Category; ::_thesis: for T being Functor of C,D
for c being Object of C holds T . (id c) = id ((Obj T) . c)
let T be Functor of C,D; ::_thesis: for c being Object of C holds T . (id c) = id ((Obj T) . c)
let c be Object of C; ::_thesis: T . (id c) = id ((Obj T) . c)
 ex d being Object of D st T . (id c) = id d by Def15;
hence  T . (id c) = id ((Obj T) . c) by Th67; ::_thesis: verum
end;

theorem Th69: :: CAT_1:69
for C, D being Category
for T being Functor of C,D
for f being Morphism of C holds
( (Obj T) . (dom f) = dom (T . f) & (Obj T) . (cod f) = cod (T . f) )
proof
let C, D be Category; ::_thesis: for T being Functor of C,D
for f being Morphism of C holds
( (Obj T) . (dom f) = dom (T . f) & (Obj T) . (cod f) = cod (T . f) )
let T be Functor of C,D; ::_thesis: for f being Morphism of C holds
( (Obj T) . (dom f) = dom (T . f) & (Obj T) . (cod f) = cod (T . f) )
let f be Morphism of C; ::_thesis: ( (Obj T) . (dom f) = dom (T . f) & (Obj T) . (cod f) = cod (T . f) )
 ( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) ) by Def15;
hence  ( (Obj T) . (dom f) = dom (T . f) & (Obj T) . (cod f) = cod (T . f) ) by Th67; ::_thesis: verum
end;

definition
let C, D be Category;
let T be Functor of C,D;
let c be Object of C;
funcT . c ->  Object of D equals :: CAT_1:def 23
(Obj T) . c;
correctness
coherence
(Obj T) . c is Object of D;
;
end;

:: deftheorem  defines . CAT_1:def_23_:_
 for C, D being Category
for T being Functor of C,D
for c being Object of C holds T . c = (Obj T) . c;

theorem :: CAT_1:70
for C, D being Category
for T being Functor of C,D
for c being Object of C
for d being Object of D st T . (id c) = id d holds
T . c = d by Th67;

theorem :: CAT_1:71
for C, D being Category
for T being Functor of C,D
for c being Object of C holds T . (id c) = id (T . c) by Th68;

theorem :: CAT_1:72
for C, D being Category
for T being Functor of C,D
for f being Morphism of C holds
( T . (dom f) = dom (T . f) & T . (cod f) = cod (T . f) ) by Th69;

theorem Th73: :: CAT_1:73
for B, C, D being Category
for T being Functor of B,C
for S being Functor of C,D holds S * T is Functor of B,D
proof
let B, C, D be Category; ::_thesis: for T being Functor of B,C
for S being Functor of C,D holds S * T is Functor of B,D
let T be Functor of B,C; ::_thesis: for S being Functor of C,D holds S * T is Functor of B,D
let S be Functor of C,D; ::_thesis: S * T is Functor of B,D
reconsider FF = (Obj S) * (Obj T) as Function of the carrier of B, the carrier of D ;
reconsider TT = S * T as Function of the carrier' of B, the carrier' of D ;
now__::_thesis:_(_(_for_b_being_Object_of_B_holds_TT_._(id_b)_=_id_(FF_._b)_)_&_(_for_f_being_Morphism_of_B_holds_
(_FF_._(dom_f)_=_dom_(TT_._f)_&_FF_._(cod_f)_=_cod_(TT_._f)_)_)_&_(_for_f,_g_being_Morphism_of_B_st_dom_g_=_cod_f_holds_
TT_._(g_(*)_f)_=_(TT_._g)_(*)_(TT_._f)_)_)
thus  for b being Object of B holds TT . (id b) = id (FF . b) ::_thesis: ( ( for f being Morphism of B holds
( FF . (dom f) = dom (TT . f) & FF . (cod f) = cod (TT . f) ) ) & ( for f, g being Morphism of B st dom g = cod f holds
TT . (g (*) f) = (TT . g) (*) (TT . f) ) )
proof
let b be Object of B; ::_thesis: TT . (id b) = id (FF . b)
thus TT . (id b) = S . (T . (id b)) by FUNCT_2:15
.= S . (id (T . b)) by Th68
.= id (S . ((Obj T) . b)) by Th68
.= id (FF . b) by FUNCT_2:15 ; ::_thesis: verum
end;
thus  for f being Morphism of B holds
( FF . (dom f) = dom (TT . f) & FF . (cod f) = cod (TT . f) ) ::_thesis: for f, g being Morphism of B st dom g = cod f holds
TT . (g (*) f) = (TT . g) (*) (TT . f)
proof
let f be Morphism of B; ::_thesis: ( FF . (dom f) = dom (TT . f) & FF . (cod f) = cod (TT . f) )
thus FF . (dom f) = (Obj S) . ((Obj T) . (dom f)) by FUNCT_2:15
.= (Obj S) . (dom (T . f)) by Th69
.= dom (S . (T . f)) by Th69
.= dom (TT . f) by FUNCT_2:15 ; ::_thesis: FF . (cod f) = cod (TT . f)
thus FF . (cod f) = (Obj S) . ((Obj T) . (cod f)) by FUNCT_2:15
.= (Obj S) . (cod (T . f)) by Th69
.= cod (S . (T . f)) by Th69
.= cod (TT . f) by FUNCT_2:15 ; ::_thesis: verum
end;
let f, g be Morphism of B; ::_thesis: ( dom g = cod f implies TT . (g (*) f) = (TT . g) (*) (TT . f) )
assume A1: dom g = cod f ; ::_thesis: TT . (g (*) f) = (TT . g) (*) (TT . f)
then A2: dom (T . g) = cod (T . f) by Th64;
thus TT . (g (*) f) = S . (T . (g (*) f)) by FUNCT_2:15
.= S . ((T . g) (*) (T . f)) by A1, Th64
.= (S . (T . g)) (*) (S . (T . f)) by A2, Th64
.= (TT . g) (*) (S . (T . f)) by FUNCT_2:15
.= (TT . g) (*) (TT . f) by FUNCT_2:15 ; ::_thesis: verum
end;
hence  S * T is Functor of B,D by Th65; ::_thesis: verum
end;

definition
let B, C, D be Category;
let T be Functor of B,C;
let S be Functor of C,D;
:: original: *
redefine funcS * T ->  Functor of B,D;
coherence
 T * S is Functor of B,D by Th73;
end;

theorem Th74: :: CAT_1:74
for C being Category holds id the carrier' of C is Functor of C,C
proof
let C be Category; ::_thesis: id the carrier' of C is Functor of C,C
set F = id the carrier of C;
set T = id the carrier' of C;
now__::_thesis:_(_(_for_c_being_Object_of_C_holds_(id_the_carrier'_of_C)_._(id_c)_=_id_((id_the_carrier_of_C)_._c)_)_&_(_for_f_being_Morphism_of_C_holds_
(_(id_the_carrier_of_C)_._(dom_f)_=_dom_((id_the_carrier'_of_C)_._f)_&_(id_the_carrier_of_C)_._(cod_f)_=_cod_((id_the_carrier'_of_C)_._f)_)_)_&_(_for_f,_g_being_Morphism_of_C_st_dom_g_=_cod_f_holds_
(id_the_carrier'_of_C)_._(g_(*)_f)_=_((id_the_carrier'_of_C)_._g)_(*)_((id_the_carrier'_of_C)_._f)_)_)
thus  for c being Object of C holds (id the carrier' of C) . (id c) = id ((id the carrier of C) . c) ::_thesis: ( ( for f being Morphism of C holds
( (id the carrier of C) . (dom f) = dom ((id the carrier' of C) . f) & (id the carrier of C) . (cod f) = cod ((id the carrier' of C) . f) ) ) & ( for f, g being Morphism of C st dom g = cod f holds
(id the carrier' of C) . (g (*) f) = ((id the carrier' of C) . g) (*) ((id the carrier' of C) . f) ) )
proof
let c be Object of C; ::_thesis: (id the carrier' of C) . (id c) = id ((id the carrier of C) . c)
 (id the carrier of C) . c = c by FUNCT_1:18;
hence  (id the carrier' of C) . (id c) = id ((id the carrier of C) . c) by FUNCT_1:18; ::_thesis: verum
end;
thus  for f being Morphism of C holds
( (id the carrier of C) . (dom f) = dom ((id the carrier' of C) . f) & (id the carrier of C) . (cod f) = cod ((id the carrier' of C) . f) ) ::_thesis: for f, g being Morphism of C st dom g = cod f holds
(id the carrier' of C) . (g (*) f) = ((id the carrier' of C) . g) (*) ((id the carrier' of C) . f)
proof
let f be Morphism of C; ::_thesis: ( (id the carrier of C) . (dom f) = dom ((id the carrier' of C) . f) & (id the carrier of C) . (cod f) = cod ((id the carrier' of C) . f) )
 (id the carrier' of C) . f = f by FUNCT_1:18;
hence  ( (id the carrier of C) . (dom f) = dom ((id the carrier' of C) . f) & (id the carrier of C) . (cod f) = cod ((id the carrier' of C) . f) ) by FUNCT_1:18; ::_thesis: verum
end;
let f, g be Morphism of C; ::_thesis: ( dom g = cod f implies (id the carrier' of C) . (g (*) f) = ((id the carrier' of C) . g) (*) ((id the carrier' of C) . f) )
assume  dom g = cod f ; ::_thesis: (id the carrier' of C) . (g (*) f) = ((id the carrier' of C) . g) (*) ((id the carrier' of C) . f)
thus (id the carrier' of C) . (g (*) f) = g (*) f by FUNCT_1:18
.= ((id the carrier' of C) . g) (*) f by FUNCT_1:18
.= ((id the carrier' of C) . g) (*) ((id the carrier' of C) . f) by FUNCT_1:18 ; ::_thesis: verum
end;
hence  id the carrier' of C is Functor of C,C by Th65; ::_thesis: verum
end;

theorem Th75: :: CAT_1:75
for B, C, D being Category
for T being Functor of B,C
for S being Functor of C,D
for b being Object of B holds (Obj (S * T)) . b = (Obj S) . ((Obj T) . b)
proof
let B, C, D be Category; ::_thesis: for T being Functor of B,C
for S being Functor of C,D
for b being Object of B holds (Obj (S * T)) . b = (Obj S) . ((Obj T) . b)
let T be Functor of B,C; ::_thesis: for S being Functor of C,D
for b being Object of B holds (Obj (S * T)) . b = (Obj S) . ((Obj T) . b)
let S be Functor of C,D; ::_thesis: for b being Object of B holds (Obj (S * T)) . b = (Obj S) . ((Obj T) . b)
let b be Object of B; ::_thesis: (Obj (S * T)) . b = (Obj S) . ((Obj T) . b)
A1: (S * T) . (id b) = S . (T . (id b)) by FUNCT_2:15;
consider d being Object of D such that
A2: (S * T) . (id b) = id d by Def15;
consider c being Object of C such that
A3: T . (id b) = id c by Def15;
thus (Obj (S * T)) . b = d by A2, Th67
.= (Obj S) . c by A2, A3, A1, Th67
.= (Obj S) . ((Obj T) . b) by A3, Th67 ; ::_thesis: verum
end;

theorem :: CAT_1:76
for B, C, D being Category
for T being Functor of B,C
for S being Functor of C,D
for b being Object of B holds (S * T) . b = S . (T . b) by Th75;

definition
let C be Category;
func id C ->  Functor of C,C equals :: CAT_1:def 24
 id the carrier' of C;
coherence
 id the carrier' of C is Functor of C,C by Th74;
end;

:: deftheorem  defines id CAT_1:def_24_:_
 for C being Category holds id C = id the carrier' of C;

theorem Th77: :: CAT_1:77
for C being Category
for c being Object of C holds (Obj (id C)) . c = c
proof
let C be Category; ::_thesis: for c being Object of C holds (Obj (id C)) . c = c
let c be Object of C; ::_thesis: (Obj (id C)) . c = c
 (id C) . (id c) = id c by FUNCT_1:18;
hence  (Obj (id C)) . c = c by Th67; ::_thesis: verum
end;

theorem Th78: :: CAT_1:78
for C being Category holds Obj (id C) = id the carrier of C
proof
let C be Category; ::_thesis: Obj (id C) = id the carrier of C
 ( dom (Obj (id C)) = the carrier of C & ( for x being set st x in the carrier of C holds
(Obj (id C)) . x = x ) ) by Th77, FUNCT_2:def_1;
hence  Obj (id C) = id the carrier of C by FUNCT_1:17; ::_thesis: verum
end;

theorem :: CAT_1:79
for C being Category
for c being Object of C holds (id C) . c = c by Th77;

definition
let C, D be Category;
let T be Functor of C,D;
attrT is isomorphic  means :: CAT_1:def 25
( T is one-to-one & rng T = the carrier' of D & rng (Obj T) = the carrier of D );
attrT is full  means :Def20: :: CAT_1:def 26
 for c, c9 being Object of C st Hom ((T . c),(T . c9)) <> {} holds
for g being Morphism of T . c,T . c9 holds
( Hom (c,c9) <> {} & ex f being Morphism of c,c9 st g = T . f );
attrT is faithful  means :Def21: :: CAT_1:def 27
 for c, c9 being Object of C st Hom (c,c9) <> {} holds
for f1, f2 being Morphism of c,c9 st T . f1 = T . f2 holds
f1 = f2;
end;

:: deftheorem  defines isomorphic CAT_1:def_25_:_
 for C, D being Category
for T being Functor of C,D holds
( T is isomorphic iff ( T is one-to-one & rng T = the carrier' of D & rng (Obj T) = the carrier of D ) );

:: deftheorem Def20 defines full CAT_1:def_26_:_
 for C, D being Category
for T being Functor of C,D holds
( T is full iff for c, c9 being Object of C st Hom ((T . c),(T . c9)) <> {} holds
for g being Morphism of T . c,T . c9 holds
( Hom (c,c9) <> {} & ex f being Morphism of c,c9 st g = T . f ) );

:: deftheorem Def21 defines faithful CAT_1:def_27_:_
 for C, D being Category
for T being Functor of C,D holds
( T is faithful iff for c, c9 being Object of C st Hom (c,c9) <> {} holds
for f1, f2 being Morphism of c,c9 st T . f1 = T . f2 holds
f1 = f2 );

theorem :: CAT_1:80
for C being Category holds id C is isomorphic
proof
let C be Category; ::_thesis: id C is isomorphic
 rng (id the carrier of C) = the carrier of C ;
hence  ( id C is one-to-one & rng (id C) = the carrier' of C & rng (Obj (id C)) = the carrier of C ) by Th78, RELAT_1:45; :: according to CAT_1:def_25 ::_thesis: verum
end;

theorem Th81: :: CAT_1:81
for C, D being Category
for T being Functor of C,D
for c, c9 being Object of C
for f being set st f in Hom (c,c9) holds
T . f in Hom ((T . c),(T . c9))
proof
let C, D be Category; ::_thesis: for T being Functor of C,D
for c, c9 being Object of C
for f being set st f in Hom (c,c9) holds
T . f in Hom ((T . c),(T . c9))
let T be Functor of C,D; ::_thesis: for c, c9 being Object of C
for f being set st f in Hom (c,c9) holds
T . f in Hom ((T . c),(T . c9))
let c, c9 be Object of C; ::_thesis: for f being set st f in Hom (c,c9) holds
T . f in Hom ((T . c),(T . c9))
let f be set ; ::_thesis: ( f in Hom (c,c9) implies T . f in Hom ((T . c),(T . c9)) )
assume A1: f in Hom (c,c9) ; ::_thesis: T . f in Hom ((T . c),(T . c9))
then reconsider f9 = f as Morphism of c,c9 by Def4;
 cod f9 = c9 by A1, Th1;
then A2: T . c9 = cod (T . f9) by Th69;
 dom f9 = c by A1, Th1;
then  T . c = dom (T . f9) by Th69;
hence  T . f in Hom ((T . c),(T . c9)) by A2; ::_thesis: verum
end;

theorem Th82: :: CAT_1:82
for C, D being Category
for T being Functor of C,D
for c, c9 being Object of C st Hom (c,c9) <> {} holds
for f being Morphism of c,c9 holds T . f in Hom ((T . c),(T . c9))
proof
let C, D be Category; ::_thesis: for T being Functor of C,D
for c, c9 being Object of C st Hom (c,c9) <> {} holds
for f being Morphism of c,c9 holds T . f in Hom ((T . c),(T . c9))
let T be Functor of C,D; ::_thesis: for c, c9 being Object of C st Hom (c,c9) <> {} holds
for f being Morphism of c,c9 holds T . f in Hom ((T . c),(T . c9))
let c, c9 be Object of C; ::_thesis: ( Hom (c,c9) <> {} implies for f being Morphism of c,c9 holds T . f in Hom ((T . c),(T . c9)) )
assume A1: Hom (c,c9) <> {} ; ::_thesis: for f being Morphism of c,c9 holds T . f in Hom ((T . c),(T . c9))
let f be Morphism of c,c9; ::_thesis: T . f in Hom ((T . c),(T . c9))
 f in Hom (c,c9) by A1, Def4;
hence  T . f in Hom ((T . c),(T . c9)) by Th81; ::_thesis: verum
end;

theorem Th83: :: CAT_1:83
for C, D being Category
for T being Functor of C,D
for c, c9 being Object of C st Hom (c,c9) <> {} holds
for f being Morphism of c,c9 holds T . f is Morphism of T . c,T . c9
proof
let C, D be Category; ::_thesis: for T being Functor of C,D
for c, c9 being Object of C st Hom (c,c9) <> {} holds
for f being Morphism of c,c9 holds T . f is Morphism of T . c,T . c9
let T be Functor of C,D; ::_thesis: for c, c9 being Object of C st Hom (c,c9) <> {} holds
for f being Morphism of c,c9 holds T . f is Morphism of T . c,T . c9
let c, c9 be Object of C; ::_thesis: ( Hom (c,c9) <> {} implies for f being Morphism of c,c9 holds T . f is Morphism of T . c,T . c9 )
assume A1: Hom (c,c9) <> {} ; ::_thesis: for f being Morphism of c,c9 holds T . f is Morphism of T . c,T . c9
let f be Morphism of c,c9; ::_thesis: T . f is Morphism of T . c,T . c9
 T . f in Hom ((T . c),(T . c9)) by A1, Th82;
hence  T . f is Morphism of T . c,T . c9 by Def4; ::_thesis: verum
end;

theorem Th84: :: CAT_1:84
for C, D being Category
for T being Functor of C,D
for c, c9 being Object of C st Hom (c,c9) <> {} holds
Hom ((T . c),(T . c9)) <> {}
proof
let C, D be Category; ::_thesis: for T being Functor of C,D
for c, c9 being Object of C st Hom (c,c9) <> {} holds
Hom ((T . c),(T . c9)) <> {}
let T be Functor of C,D; ::_thesis: for c, c9 being Object of C st Hom (c,c9) <> {} holds
Hom ((T . c),(T . c9)) <> {}
let c, c9 be Object of C; ::_thesis: ( Hom (c,c9) <> {} implies Hom ((T . c),(T . c9)) <> {} )
set f = the Element of Hom (c,c9);
assume  Hom (c,c9) <> {} ; ::_thesis: Hom ((T . c),(T . c9)) <> {}
then  the Element of Hom (c,c9) in Hom (c,c9) ;
hence  Hom ((T . c),(T . c9)) <> {} by Th81; ::_thesis: verum
end;

theorem :: CAT_1:85
for B, C, D being Category
for T being Functor of B,C
for S being Functor of C,D st T is full & S is full holds
S * T is full
proof
let B, C, D be Category; ::_thesis: for T being Functor of B,C
for S being Functor of C,D st T is full & S is full holds
S * T is full
let T be Functor of B,C; ::_thesis: for S being Functor of C,D st T is full & S is full holds
S * T is full
let S be Functor of C,D; ::_thesis: ( T is full & S is full implies S * T is full )
assume that
A1: T is full and
A2: S is full ; ::_thesis: S * T is full
let b, b9 be Object of B; :: according to CAT_1:def_26 ::_thesis: ( Hom (((S * T) . b),((S * T) . b9)) <> {} implies for g being Morphism of (S * T) . b,(S * T) . b9 holds
( Hom (b,b9) <> {} & ex f being Morphism of b,b9 st g = (S * T) . f ) )
assume A3: Hom (((S * T) . b),((S * T) . b9)) <> {} ; ::_thesis: for g being Morphism of (S * T) . b,(S * T) . b9 holds
( Hom (b,b9) <> {} & ex f being Morphism of b,b9 st g = (S * T) . f )
let g be Morphism of (S * T) . b,(S * T) . b9; ::_thesis: ( Hom (b,b9) <> {} & ex f being Morphism of b,b9 st g = (S * T) . f )
A4: ( (S * T) . b = S . (T . b) & (S * T) . b9 = S . (T . b9) ) by Th75;
then consider f being Morphism of T . b,T . b9 such that
A5: g = S . f by A2, A3, Def20;
A6: Hom ((T . b),(T . b9)) <> {} by A2, A3, A4, Def20;
hence  Hom (b,b9) <> {} by A1, Def20; ::_thesis: ex f being Morphism of b,b9 st g = (S * T) . f
consider h being Morphism of b,b9 such that
A7: f = T . h by A1, A6, Def20;
take  h ; ::_thesis: g = (S * T) . h
thus  g = (S * T) . h by A5, A7, FUNCT_2:15; ::_thesis: verum
end;

theorem :: CAT_1:86
for B, C, D being Category
for T being Functor of B,C
for S being Functor of C,D st T is faithful & S is faithful holds
S * T is faithful
proof
let B, C, D be Category; ::_thesis: for T being Functor of B,C
for S being Functor of C,D st T is faithful & S is faithful holds
S * T is faithful
let T be Functor of B,C; ::_thesis: for S being Functor of C,D st T is faithful & S is faithful holds
S * T is faithful
let S be Functor of C,D; ::_thesis: ( T is faithful & S is faithful implies S * T is faithful )
assume that
A1: T is faithful and
A2: S is faithful ; ::_thesis: S * T is faithful
let b, b9 be Object of B; :: according to CAT_1:def_27 ::_thesis: ( Hom (b,b9) <> {} implies for f1, f2 being Morphism of b,b9 st (S * T) . f1 = (S * T) . f2 holds
f1 = f2 )
assume A3: Hom (b,b9) <> {} ; ::_thesis: for f1, f2 being Morphism of b,b9 st (S * T) . f1 = (S * T) . f2 holds
f1 = f2
let f1, f2 be Morphism of b,b9; ::_thesis: ( (S * T) . f1 = (S * T) . f2 implies f1 = f2 )
A4: T . f2 is Morphism of T . b,T . b9 by A3, Th83;
assume A5: (S * T) . f1 = (S * T) . f2 ; ::_thesis: f1 = f2
A6: ( (S * T) . f1 = S . (T . f1) & (S * T) . f2 = S . (T . f2) ) by FUNCT_2:15;
 ( Hom ((T . b),(T . b9)) <> {} & T . f1 is Morphism of T . b,T . b9 ) by A3, Th83, Th84;
then  T . f1 = T . f2 by A2, A5, A6, A4, Def21;
hence  f1 = f2 by A1, A3, Def21; ::_thesis: verum
end;

theorem Th87: :: CAT_1:87
for C, D being Category
for T being Functor of C,D
for c, c9 being Object of C holds T .: (Hom (c,c9)) c= Hom ((T . c),(T . c9))
proof
let C, D be Category; ::_thesis: for T being Functor of C,D
for c, c9 being Object of C holds T .: (Hom (c,c9)) c= Hom ((T . c),(T . c9))
let T be Functor of C,D; ::_thesis: for c, c9 being Object of C holds T .: (Hom (c,c9)) c= Hom ((T . c),(T . c9))
let c, c9 be Object of C; ::_thesis: T .: (Hom (c,c9)) c= Hom ((T . c),(T . c9))
let f be set ; :: according to TARSKI:def_3 ::_thesis: ( not f in T .: (Hom (c,c9)) or f in Hom ((T . c),(T . c9)) )
assume  f in T .: (Hom (c,c9)) ; ::_thesis: f in Hom ((T . c),(T . c9))
then  ex g being Element of the carrier' of C st
( g in Hom (c,c9) & f = T . g ) by FUNCT_2:65;
hence  f in Hom ((T . c),(T . c9)) by Th81; ::_thesis: verum
end;

definition
let C, D be Category;
let T be Functor of C,D;
let c, c9 be Object of C;
func hom (T,c,c9) ->  Function of (Hom (c,c9)),(Hom ((T . c),(T . c9))) equals :: CAT_1:def 28
T | (Hom (c,c9));
correctness
coherence
T | (Hom (c,c9)) is Function of (Hom (c,c9)),(Hom ((T . c),(T . c9)));
proof
 T .: (Hom (c,c9)) c= Hom ((T . c),(T . c9)) by Th87;
hence  T | (Hom (c,c9)) is Function of (Hom (c,c9)),(Hom ((T . c),(T . c9))) by FUNCT_2:101; ::_thesis: verum
end;
end;

:: deftheorem  defines hom CAT_1:def_28_:_
 for C, D being Category
for T being Functor of C,D
for c, c9 being Object of C holds hom (T,c,c9) = T | (Hom (c,c9));

theorem Th88: :: CAT_1:88
for C, D being Category
for T being Functor of C,D
for c, c9 being Object of C st Hom (c,c9) <> {} holds
for f being Morphism of c,c9 holds (hom (T,c,c9)) . f = T . f
proof
let C, D be Category; ::_thesis: for T being Functor of C,D
for c, c9 being Object of C st Hom (c,c9) <> {} holds
for f being Morphism of c,c9 holds (hom (T,c,c9)) . f = T . f
let T be Functor of C,D; ::_thesis: for c, c9 being Object of C st Hom (c,c9) <> {} holds
for f being Morphism of c,c9 holds (hom (T,c,c9)) . f = T . f
let c, c9 be Object of C; ::_thesis: ( Hom (c,c9) <> {} implies for f being Morphism of c,c9 holds (hom (T,c,c9)) . f = T . f )
assume A1: Hom (c,c9) <> {} ; ::_thesis: for f being Morphism of c,c9 holds (hom (T,c,c9)) . f = T . f
let f be Morphism of c,c9; ::_thesis: (hom (T,c,c9)) . f = T . f
 f in Hom (c,c9) by A1, Def4;
hence  (hom (T,c,c9)) . f = T . f by FUNCT_1:49; ::_thesis: verum
end;

theorem :: CAT_1:89
for C, D being Category
for T being Functor of C,D holds
( T is full iff for c, c9 being Object of C holds rng (hom (T,c,c9)) = Hom ((T . c),(T . c9)) )
proof
let C, D be Category; ::_thesis: for T being Functor of C,D holds
( T is full iff for c, c9 being Object of C holds rng (hom (T,c,c9)) = Hom ((T . c),(T . c9)) )
let T be Functor of C,D; ::_thesis: ( T is full iff for c, c9 being Object of C holds rng (hom (T,c,c9)) = Hom ((T . c),(T . c9)) )
thus  ( T is full implies for c, c9 being Object of C holds rng (hom (T,c,c9)) = Hom ((T . c),(T . c9)) ) ::_thesis: ( ( for c, c9 being Object of C holds rng (hom (T,c,c9)) = Hom ((T . c),(T . c9)) ) implies T is full )
proof
assume A1: T is full ; ::_thesis: for c, c9 being Object of C holds rng (hom (T,c,c9)) = Hom ((T . c),(T . c9))
let c, c9 be Object of C; ::_thesis: rng (hom (T,c,c9)) = Hom ((T . c),(T . c9))
now__::_thesis:_(_Hom_((T_._c),(T_._c9))_<>_{}_implies_rng_(hom_(T,c,c9))_=_Hom_((T_._c),(T_._c9))_)
assume A2: Hom ((T . c),(T . c9)) <> {} ; ::_thesis: rng (hom (T,c,c9)) = Hom ((T . c),(T . c9))
 for g being set holds
( g in rng (hom (T,c,c9)) iff g in Hom ((T . c),(T . c9)) )
proof
let g be set ; ::_thesis: ( g in rng (hom (T,c,c9)) iff g in Hom ((T . c),(T . c9)) )
thus  ( g in rng (hom (T,c,c9)) implies g in Hom ((T . c),(T . c9)) ) ::_thesis: ( g in Hom ((T . c),(T . c9)) implies g in rng (hom (T,c,c9)) )
proof
assume  g in rng (hom (T,c,c9)) ; ::_thesis: g in Hom ((T . c),(T . c9))
then consider f being set  such that
A3: f in dom (hom (T,c,c9)) and
A4: (hom (T,c,c9)) . f = g by FUNCT_1:def_3;
 f in Hom (c,c9) by A2, A3, FUNCT_2:def_1;
hence  g in Hom ((T . c),(T . c9)) by A2, A4, FUNCT_2:5; ::_thesis: verum
end;
assume  g in Hom ((T . c),(T . c9)) ; ::_thesis: g in rng (hom (T,c,c9))
then  g is Morphism of T . c,T . c9 by Def4;
then consider f being Morphism of c,c9 such that
A5: g = T . f by A1, A2, Def20;
 Hom (c,c9) <> {} by A1, A2, Def20;
then  f in Hom (c,c9) by Def4;
then  (hom (T,c,c9)) . f in rng (hom (T,c,c9)) by A2, FUNCT_2:4;
hence  g in rng (hom (T,c,c9)) by A5, A1, A2, Def20, Th88; ::_thesis: verum
end;
hence  rng (hom (T,c,c9)) = Hom ((T . c),(T . c9)) by TARSKI:1; ::_thesis: verum
end;
hence  rng (hom (T,c,c9)) = Hom ((T . c),(T . c9)) ; ::_thesis: verum
end;
assume A7: for c, c9 being Object of C holds rng (hom (T,c,c9)) = Hom ((T . c),(T . c9)) ; ::_thesis: T is full
let c, c9 be Object of C; :: according to CAT_1:def_26 ::_thesis: ( Hom ((T . c),(T . c9)) <> {} implies for g being Morphism of T . c,T . c9 holds
( Hom (c,c9) <> {} & ex f being Morphism of c,c9 st g = T . f ) )
assume A8: Hom ((T . c),(T . c9)) <> {} ; ::_thesis: for g being Morphism of T . c,T . c9 holds
( Hom (c,c9) <> {} & ex f being Morphism of c,c9 st g = T . f )
let g be Morphism of T . c,T . c9; ::_thesis: ( Hom (c,c9) <> {} & ex f being Morphism of c,c9 st g = T . f )
 g in Hom ((T . c),(T . c9)) by A8, Def4;
then  g in rng (hom (T,c,c9)) by A7;
then consider f being set  such that
A9: f in dom (hom (T,c,c9)) and
A10: (hom (T,c,c9)) . f = g by FUNCT_1:def_3;
thus  Hom (c,c9) <> {} by A9; ::_thesis: ex f being Morphism of c,c9 st g = T . f
A11: f in Hom (c,c9) by A8, A9, FUNCT_2:def_1;
then reconsider f = f as Morphism of c,c9 by Def4;
take  f ; ::_thesis: g = T . f
thus  g = T . f by A10, A11, Th88; ::_thesis: verum
end;

theorem :: CAT_1:90
for C, D being Category
for T being Functor of C,D holds
( T is faithful iff for c, c9 being Object of C holds hom (T,c,c9) is one-to-one )
proof
let C, D be Category; ::_thesis: for T being Functor of C,D holds
( T is faithful iff for c, c9 being Object of C holds hom (T,c,c9) is one-to-one )
let T be Functor of C,D; ::_thesis: ( T is faithful iff for c, c9 being Object of C holds hom (T,c,c9) is one-to-one )
thus  ( T is faithful implies for c, c9 being Object of C holds hom (T,c,c9) is one-to-one ) ::_thesis: ( ( for c, c9 being Object of C holds hom (T,c,c9) is one-to-one ) implies T is faithful )
proof
assume A1: T is faithful ; ::_thesis: for c, c9 being Object of C holds hom (T,c,c9) is one-to-one
let c, c9 be Object of C; ::_thesis: hom (T,c,c9) is one-to-one
now__::_thesis:_(_Hom_((T_._c),(T_._c9))_<>_{}_implies_hom_(T,c,c9)_is_one-to-one_)
A2: now__::_thesis:_for_f1,_f2_being_set_st_f1_in_Hom_(c,c9)_&_f2_in_Hom_(c,c9)_&_(hom_(T,c,c9))_._f1_=_(hom_(T,c,c9))_._f2_holds_
f1_=_f2
let f1, f2 be set ; ::_thesis: ( f1 in Hom (c,c9) & f2 in Hom (c,c9) & (hom (T,c,c9)) . f1 = (hom (T,c,c9)) . f2 implies f1 = f2 )
assume that
A3: f1 in Hom (c,c9) and
A4: f2 in Hom (c,c9) ; ::_thesis: ( (hom (T,c,c9)) . f1 = (hom (T,c,c9)) . f2 implies f1 = f2 )
A5: f2 is Morphism of c,c9 by A4, Def4;
then A6: T . f2 = (hom (T,c,c9)) . f2 by A3, Th88;
A7: f1 is Morphism of c,c9 by A3, Def4;
then  T . f1 = (hom (T,c,c9)) . f1 by A3, Th88;
hence  ( (hom (T,c,c9)) . f1 = (hom (T,c,c9)) . f2 implies f1 = f2 ) by A1, A3, A7, A5, A6, Def21; ::_thesis: verum
end;
assume  Hom ((T . c),(T . c9)) <> {} ; ::_thesis: hom (T,c,c9) is one-to-one
hence  hom (T,c,c9) is one-to-one by A2, FUNCT_2:19; ::_thesis: verum
end;
hence  hom (T,c,c9) is one-to-one ; ::_thesis: verum
end;
assume A8: for c, c9 being Object of C holds hom (T,c,c9) is one-to-one ; ::_thesis: T is faithful
let c, c9 be Object of C; :: according to CAT_1:def_27 ::_thesis: ( Hom (c,c9) <> {} implies for f1, f2 being Morphism of c,c9 st T . f1 = T . f2 holds
f1 = f2 )
assume A9: Hom (c,c9) <> {} ; ::_thesis: for f1, f2 being Morphism of c,c9 st T . f1 = T . f2 holds
f1 = f2
let f1, f2 be Morphism of c,c9; ::_thesis: ( T . f1 = T . f2 implies f1 = f2 )
A10: T . f2 = (hom (T,c,c9)) . f2 by A9, Th88;
A11: ( f2 in Hom (c,c9) & T . f1 = (hom (T,c,c9)) . f1 ) by A9, Def4, Th88;
A12: hom (T,c,c9) is one-to-one by A8;
 ( Hom ((T . c),(T . c9)) <> {} & f1 in Hom (c,c9) ) by A9, Def4, Th84;
hence  ( T . f1 = T . f2 implies f1 = f2 ) by A12, A11, A10, FUNCT_2:19; ::_thesis: verum
end;