:: CAT_1 semantic presentation

theorem Th1: :: CAT_1:1
canceled;

theorem Th2: :: CAT_1:2
canceled;

theorem Th3: :: CAT_1:3
canceled;

theorem Th4: :: CAT_1:4
for b1, b2, b3 being set
for b4 being non empty set
for b5 being Function of b1,b4 st b2 c= b1 & b5 .: b2 c= b3 holds
b5 | b2 is Function of b2,b3
proof end;

definition
let c1, c2, c3 be set ;
func c1,c2 .--> c3 -> PartFunc of [:{a1},{a2}:],{a3} equals :: CAT_1:def 1
[a1,a2] .--> a3;
correctness
coherence
[c1,c2] .--> c3 is PartFunc of [:{c1},{c2}:],{c3};
proof end;
end;

:: deftheorem Def1 defines .--> CAT_1:def 1 :
for b1, b2, b3 being set holds b1,b2 .--> b3 = [b1,b2] .--> b3;

theorem Th5: :: CAT_1:5
canceled;

theorem Th6: :: CAT_1:6
canceled;

theorem Th7: :: CAT_1:7
for b1, b2, b3 being set holds
( dom (b1,b2 .--> b3) = {[b1,b2]} & dom (b1,b2 .--> b3) = [:{b1},{b2}:] )
proof end;

theorem Th8: :: CAT_1:8
for b1, b2, b3 being set holds (b1,b2 .--> b3) . [b1,b2] = b3
proof end;

theorem Th9: :: CAT_1:9
for b1, b2, b3 being set
for b4 being Element of {b1}
for b5 being Element of {b2} holds (b1,b2 .--> b3) . [b4,b5] = b3
proof end;

definition
attr a1 is strict;
struct CatStr -> ;
aggr CatStr(# Objects, Morphisms, Dom, Cod, Comp, Id #) -> CatStr ;
sel Objects c1 -> non empty set ;
sel Morphisms c1 -> non empty set ;
sel Dom c1 -> Function of the Morphisms of a1,the Objects of a1;
sel Cod c1 -> Function of the Morphisms of a1,the Objects of a1;
sel Comp c1 -> PartFunc of [:the Morphisms of a1,the Morphisms of a1:],the Morphisms of a1;
sel Id c1 -> Function of the Objects of a1,the Morphisms of a1;
end;

definition
let c1 be CatStr ;
mode Object of a1 is Element of the Objects of a1;
mode Morphism of a1 is Element of the Morphisms of a1;
end;

definition
let c1 be CatStr ;
let c2 be Morphism of c1;
func dom c2 -> Object of a1 equals :: CAT_1:def 2
the Dom of a1 . a2;
correctness
coherence
the Dom of c1 . c2 is Object of c1;
;
func cod c2 -> Object of a1 equals :: CAT_1:def 3
the Cod of a1 . a2;
correctness
coherence
the Cod of c1 . c2 is Object of c1;
;
end;

:: deftheorem Def2 defines dom CAT_1:def 2 :
for b1 being CatStr
for b2 being Morphism of b1 holds dom b2 = the Dom of b1 . b2;

:: deftheorem Def3 defines cod CAT_1:def 3 :
for b1 being CatStr
for b2 being Morphism of b1 holds cod b2 = the Cod of b1 . b2;

definition
let c1 be CatStr ;
let c2, c3 be Morphism of c1;
assume E5: [c3,c2] in dom the Comp of c1 ;
func c3 * c2 -> Morphism of a1 equals :Def4: :: CAT_1:def 4
the Comp of a1 . [a3,a2];
coherence
the Comp of c1 . [c3,c2] is Morphism of c1 by E5, PARTFUN1:27;
end;

:: deftheorem Def4 defines * CAT_1:def 4 :
for b1 being CatStr
for b2, b3 being Morphism of b1 st [b3,b2] in dom the Comp of b1 holds
b3 * b2 = the Comp of b1 . [b3,b2];

definition
let c1 be CatStr ;
let c2 be Object of c1;
func id c2 -> Morphism of a1 equals :: CAT_1:def 5
the Id of a1 . a2;
correctness
coherence
the Id of c1 . c2 is Morphism of c1;
;
end;

:: deftheorem Def5 defines id CAT_1:def 5 :
for b1 being CatStr
for b2 being Object of b1 holds id b2 = the Id of b1 . b2;

definition
let c1 be CatStr ;
let c2, c3 be Object of c1;
func Hom c2,c3 -> Subset of the Morphisms of a1 equals :: CAT_1:def 6
{ b1 where B is Morphism of a1 : ( dom b1 = a2 & cod b1 = a3 ) } ;
correctness
coherence
{ b1 where B is Morphism of c1 : ( dom b1 = c2 & cod b1 = c3 ) } is Subset of the Morphisms of c1;
proof end;
end;

:: deftheorem Def6 defines Hom CAT_1:def 6 :
for b1 being CatStr
for b2, b3 being Object of b1 holds Hom b2,b3 = { b4 where B is Morphism of b1 : ( dom b4 = b2 & cod b4 = b3 ) } ;

theorem Th10: :: CAT_1:10
canceled;

theorem Th11: :: CAT_1:11
canceled;

theorem Th12: :: CAT_1:12
canceled;

theorem Th13: :: CAT_1:13
canceled;

theorem Th14: :: CAT_1:14
canceled;

theorem Th15: :: CAT_1:15
canceled;

theorem Th16: :: CAT_1:16
canceled;

theorem Th17: :: CAT_1:17
canceled;

theorem Th18: :: CAT_1:18
for b1 being CatStr
for b2, b3 being Object of b1
for b4 being Morphism of b1 holds
( b4 in Hom b2,b3 iff ( dom b4 = b2 & cod b4 = b3 ) )
proof end;

theorem Th19: :: CAT_1:19
for b1 being CatStr
for b2 being Morphism of b1 holds Hom (dom b2),(cod b2) <> {} by Th18;

definition
let c1 be CatStr ;
let c2, c3 be Object of c1;
assume E7: Hom c2,c3 <> {} ;
mode Morphism of c2,c3 -> Morphism of a1 means :Def7: :: CAT_1:def 7
a4 in Hom a2,a3;
existence
ex b1 being Morphism of c1 st b1 in Hom c2,c3 by E7, SUBSET_1:10;
end;

:: deftheorem Def7 defines Morphism CAT_1:def 7 :
for b1 being CatStr
for b2, b3 being Object of b1 st Hom b2,b3 <> {} holds
for b4 being Morphism of b1 holds
( b4 is Morphism of b2,b3 iff b4 in Hom b2,b3 );

theorem Th20: :: CAT_1:20
canceled;

theorem Th21: :: CAT_1:21
for b1 being CatStr
for b2, b3 being Object of b1
for b4 being set st b4 in Hom b2,b3 holds
b4 is Morphism of b2,b3 by Def7;

theorem Th22: :: CAT_1:22
for b1 being CatStr
for b2 being Morphism of b1 holds b2 is Morphism of dom b2, cod b2
proof end;

theorem Th23: :: CAT_1:23
for b1 being CatStr
for b2, b3 being Object of b1
for b4 being Morphism of b2,b3 st Hom b2,b3 <> {} holds
( dom b4 = b2 & cod b4 = b3 )
proof end;

theorem Th24: :: CAT_1:24
for b1 being CatStr
for b2, b3, b4, b5 being Object of b1
for b6 being Morphism of b2,b3
for b7 being Morphism of b4,b5 st Hom b2,b3 <> {} & Hom b4,b5 <> {} & b6 = b7 holds
( b2 = b4 & b3 = b5 )
proof end;

theorem Th25: :: CAT_1:25
for b1 being CatStr
for b2, b3 being Object of b1
for b4 being Morphism of b2,b3 st Hom b2,b3 = {b4} holds
for b5 being Morphism of b2,b3 holds b4 = b5
proof end;

theorem Th26: :: CAT_1:26
for b1 being CatStr
for b2, b3 being Object of b1
for b4 being Morphism of b2,b3 st Hom b2,b3 <> {} & ( for b5 being Morphism of b2,b3 holds b4 = b5 ) holds
Hom b2,b3 = {b4}
proof end;

theorem Th27: :: CAT_1:27
for b1 being CatStr
for b2, b3, b4, b5 being Object of b1
for b6 being Morphism of b2,b3 st Hom b2,b3, Hom b4,b5 are_equipotent & Hom b2,b3 = {b6} holds
ex b7 being Morphism of b4,b5 st Hom b4,b5 = {b7}
proof end;

definition
let c1, c2 be set ;
redefine func .--> as c1 .--> c2 -> Function of {a1},{a2};
coherence
c1 .--> c2 is Function of {c1},{c2}
proof end;
end;

E12: now
let c1, c2 be set ;
let c3 be CatStr ;
assume E13: c3 = CatStr(# {c1},{c2},(c2 .--> c1),(c2 .--> c1),(c2,c2 .--> c2),(c1 .--> c2) #) ;
set c4 = the Comp of c3;
set c5 = the Dom of c3;
set c6 = the Cod of c3;
set c7 = the Id of c3;
thus for b1, b2 being Element of the Morphisms of c3 holds
( [b2,b1] in dom the Comp of c3 iff the Dom of c3 . b2 = the Cod of c3 . b1 )
proof
let c8, c9 be Element of the Morphisms of c3;
( c8 = c2 & c9 = c2 & dom the Comp of c3 = {[c2,c2]} ) by E13, Th7, TARSKI:def 1;
hence ( [c9,c8] in dom the Comp of c3 iff the Dom of c3 . c9 = the Cod of c3 . c8 ) by E13, TARSKI:def 1;
end;
thus for b1, b2 being Element of the Morphisms of c3 st the Dom of c3 . b2 = the Cod of c3 . b1 holds
( the Dom of c3 . (the Comp of c3 . [b2,b1]) = the Dom of c3 . b1 & the Cod of c3 . (the Comp of c3 . [b2,b1]) = the Cod of c3 . b2 )
proof
let c8, c9 be Element of the Morphisms of c3;
the Comp of c3 . [c9,c8] = c2 by E13, Th9;
then reconsider c10 = the Comp of c3 . [c9,c8] as Element of the Morphisms of c3 by E13, TARSKI:def 1;
( the Dom of c3 . c8 = c1 & the Cod of c3 . c9 = c1 & the Dom of c3 . c10 = c1 & the Cod of c3 . c10 = c1 ) by E13, FUNCT_2:65;
hence ( the Dom of c3 . c9 = the Cod of c3 . c8 implies ( the Dom of c3 . (the Comp of c3 . [c9,c8]) = the Dom of c3 . c8 & the Cod of c3 . (the Comp of c3 . [c9,c8]) = the Cod of c3 . c9 ) ) ;
end;
thus for b1, b2, b3 being Element of the Morphisms of c3 st the Dom of c3 . b3 = the Cod of c3 . b2 & the Dom of c3 . b2 = the Cod of c3 . b1 holds
the Comp of c3 . [b3,(the Comp of c3 . [b2,b1])] = the Comp of c3 . [(the Comp of c3 . [b3,b2]),b1]
proof
let c8, c9, c10 be Element of the Morphisms of c3;
( the Comp of c3 . [c9,c8] = c2 & the Comp of c3 . [c10,c9] = c2 ) by E13, Th9;
then reconsider c11 = the Comp of c3 . [c9,c8], c12 = the Comp of c3 . [c10,c9] as Element of the Morphisms of c3 by E13, TARSKI:def 1;
( the Comp of c3 . [c10,c11] = c2 & the Comp of c3 . [c12,c8] = c2 ) by E13, Th9;
hence ( the Dom of c3 . c10 = the Cod of c3 . c9 & the Dom of c3 . c9 = the Cod of c3 . c8 implies the Comp of c3 . [c10,(the Comp of c3 . [c9,c8])] = the Comp of c3 . [(the Comp of c3 . [c10,c9]),c8] ) ;
end;
let c8 be Element of the Objects of c3;
c8 = c1 by E13, TARSKI:def 1;
hence ( the Dom of c3 . (the Id of c3 . c8) = c8 & the Cod of c3 . (the Id of c3 . c8) = c8 ) by E13, FUNCT_2:65;
thus for b1 being Element of the Morphisms of c3 st the Cod of c3 . b1 = c8 holds
the Comp of c3 . [(the Id of c3 . c8),b1] = b1
proof
let c9 be Element of the Morphisms of c3;
c9 = c2 by E13, TARSKI:def 1;
hence ( the Cod of c3 . c9 = c8 implies the Comp of c3 . [(the Id of c3 . c8),c9] = c9 ) by E13, Th9;
end;
let c9 be Element of the Morphisms of c3;
c9 = c2 by E13, TARSKI:def 1;
hence the Comp of c3 . [c9,(the Id of c3 . c8)] = c9 by E13, Th9;
end;

definition
let c1 be CatStr ;
attr a1 is Category-like means :Def8: :: CAT_1:def 8
( ( for b1, b2 being Element of the Morphisms of a1 holds
( [b2,b1] in dom the Comp of a1 iff the Dom of a1 . b2 = the Cod of a1 . b1 ) ) & ( for b1, b2 being Element of the Morphisms of a1 st the Dom of a1 . b2 = the Cod of a1 . b1 holds
( the Dom of a1 . (the Comp of a1 . [b2,b1]) = the Dom of a1 . b1 & the Cod of a1 . (the Comp of a1 . [b2,b1]) = the Cod of a1 . b2 ) ) & ( for b1, b2, b3 being Element of the Morphisms of a1 st the Dom of a1 . b3 = the Cod of a1 . b2 & the Dom of a1 . b2 = the Cod of a1 . b1 holds
the Comp of a1 . [b3,(the Comp of a1 . [b2,b1])] = the Comp of a1 . [(the Comp of a1 . [b3,b2]),b1] ) & ( for b1 being Element of the Objects of a1 holds
( the Dom of a1 . (the Id of a1 . b1) = b1 & the Cod of a1 . (the Id of a1 . b1) = b1 & ( for b2 being Element of the Morphisms of a1 st the Cod of a1 . b2 = b1 holds
the Comp of a1 . [(the Id of a1 . b1),b2] = b2 ) & ( for b2 being Element of the Morphisms of a1 st the Dom of a1 . b2 = b1 holds
the Comp of a1 . [b2,(the Id of a1 . b1)] = b2 ) ) ) );
end;

:: deftheorem Def8 defines Category-like CAT_1:def 8 :
for b1 being CatStr holds
( b1 is Category-like iff ( ( for b2, b3 being Element of the Morphisms of b1 holds
( [b3,b2] in dom the Comp of b1 iff the Dom of b1 . b3 = the Cod of b1 . b2 ) ) & ( for b2, b3 being Element of the Morphisms of b1 st the Dom of b1 . b3 = the Cod of b1 . b2 holds
( the Dom of b1 . (the Comp of b1 . [b3,b2]) = the Dom of b1 . b2 & the Cod of b1 . (the Comp of b1 . [b3,b2]) = the Cod of b1 . b3 ) ) & ( for b2, b3, b4 being Element of the Morphisms of b1 st the Dom of b1 . b4 = the Cod of b1 . b3 & the Dom of b1 . b3 = the Cod of b1 . b2 holds
the Comp of b1 . [b4,(the Comp of b1 . [b3,b2])] = the Comp of b1 . [(the Comp of b1 . [b4,b3]),b2] ) & ( for b2 being Element of the Objects of b1 holds
( the Dom of b1 . (the Id of b1 . b2) = b2 & the Cod of b1 . (the Id of b1 . b2) = b2 & ( for b3 being Element of the Morphisms of b1 st the Cod of b1 . b3 = b2 holds
the Comp of b1 . [(the Id of b1 . b2),b3] = b3 ) & ( for b3 being Element of the Morphisms of b1 st the Dom of b1 . b3 = b2 holds
the Comp of b1 . [b3,(the Id of b1 . b2)] = b3 ) ) ) ) );

registration
cluster Category-like CatStr ;
existence
ex b1 being CatStr st b1 is Category-like
proof end;
end;

definition
mode Category is Category-like CatStr ;
end;

registration
cluster strict CatStr ;
existence
ex b1 being Category st b1 is strict
proof end;
end;

theorem Th28: :: CAT_1:28
canceled;

theorem Th29: :: CAT_1:29
for b1 being CatStr st ( for b2, b3 being Morphism of b1 holds
( [b3,b2] in dom the Comp of b1 iff dom b3 = cod b2 ) ) & ( for b2, b3 being Morphism of b1 st dom b3 = cod b2 holds
( dom (b3 * b2) = dom b2 & cod (b3 * b2) = cod b3 ) ) & ( for b2, b3, b4 being Morphism of b1 st dom b4 = cod b3 & dom b3 = cod b2 holds
b4 * (b3 * b2) = (b4 * b3) * b2 ) & ( for b2 being Object of b1 holds
( dom (id b2) = b2 & cod (id b2) = b2 & ( for b3 being Morphism of b1 st cod b3 = b2 holds
(id b2) * b3 = b3 ) & ( for b3 being Morphism of b1 st dom b3 = b2 holds
b3 * (id b2) = b3 ) ) ) holds
b1 is Category-like
proof end;

definition
let c1, c2 be set ;
func 1Cat c1,c2 -> strict Category equals :: CAT_1:def 9
 CatStr(# {a1},{a2},(a2 .--> a1),(a2 .--> a1),(a2,a2 .--> a2),(a1 .--> a2) #);
correctness
coherence
CatStr(# {c1},{c2},(c2 .--> c1),(c2 .--> c1),(c2,c2 .--> c2),(c1 .--> c2) #) is strict Category;
proof end;
end;

:: deftheorem Def9 defines 1Cat CAT_1:def 9 :
for b1, b2 being set holds 1Cat b1,b2 = CatStr(# {b1},{b2},(b2 .--> b1),(b2 .--> b1),(b2,b2 .--> b2),(b1 .--> b2) #);

theorem Th30: :: CAT_1:30
canceled;

theorem Th31: :: CAT_1:31
canceled;

theorem Th32: :: CAT_1:32
for b1, b2 being set holds b1 is Object of (1Cat b1,b2) by TARSKI:def 1;

theorem Th33: :: CAT_1:33
for b1, b2 being set holds b1 is Morphism of (1Cat b2,b1) by TARSKI:def 1;

theorem Th34: :: CAT_1:34
for b1, b2 being set
for b3 being Object of (1Cat b1,b2) holds b3 = b1 by TARSKI:def 1;

theorem Th35: :: CAT_1:35
for b1, b2 being set
for b3 being Morphism of (1Cat b1,b2) holds b3 = b2 by TARSKI:def 1;

theorem Th36: :: CAT_1:36
for b1, b2 being set
for b3, b4 being Object of (1Cat b1,b2)
for b5 being Morphism of (1Cat b1,b2) holds b5 in Hom b3,b4
proof end;

theorem Th37: :: CAT_1:37
for b1, b2 being set
for b3, b4 being Object of (1Cat b1,b2)
for b5 being Morphism of (1Cat b1,b2) holds b5 is Morphism of b3,b4
proof end;

theorem Th38: :: CAT_1:38
for b1, b2 being set
for b3, b4 being Object of (1Cat b1,b2) holds Hom b3,b4 <> {} by Th36;

theorem Th39: :: CAT_1:39
for b1, b2 being set
for b3, b4, b5, b6 being Object of (1Cat b1,b2)
for b7 being Morphism of b3,b4
for b8 being Morphism of b5,b6 holds b7 = b8
proof end;

theorem Th40: :: CAT_1:40
for b1 being Category
for b2, b3 being Morphism of b1 holds
( dom b2 = cod b3 iff [b2,b3] in dom the Comp of b1 ) by Def8;

theorem Th41: :: CAT_1:41
for b1 being Category
for b2, b3 being Morphism of b1 st dom b2 = cod b3 holds
b2 * b3 = the Comp of b1 . [b2,b3]
proof end;

theorem Th42: :: CAT_1:42
for b1 being Category
for b2, b3 being Morphism of b1 st dom b3 = cod b2 holds
( dom (b3 * b2) = dom b2 & cod (b3 * b2) = cod b3 )
proof end;

theorem Th43: :: CAT_1:43
for b1 being Category
for b2, b3, b4 being Morphism of b1 st dom b4 = cod b3 & dom b3 = cod b2 holds
b4 * (b3 * b2) = (b4 * b3) * b2
proof end;

theorem Th44: :: CAT_1:44
for b1 being Category
for b2 being Object of b1 holds
( dom (id b2) = b2 & cod (id b2) = b2 ) by Def8;

theorem Th45: :: CAT_1:45
for b1 being Category
for b2, b3 being Object of b1 st id b2 = id b3 holds
b2 = b3
proof end;

theorem Th46: :: CAT_1:46
for b1 being Category
for b2 being Object of b1
for b3 being Morphism of b1 st cod b3 = b2 holds
(id b2) * b3 = b3
proof end;

theorem Th47: :: CAT_1:47
for b1 being Category
for b2 being Object of b1
for b3 being Morphism of b1 st dom b3 = b2 holds
b3 * (id b2) = b3
proof end;

definition
let c1 be Category;
let c2 be Morphism of c1;
attr a2 is monic means :: CAT_1:def 10
for b1, b2 being Morphism of a1 st dom b1 = dom b2 & cod b1 = dom a2 & cod b2 = dom a2 & a2 * b1 = a2 * b2 holds
b1 = b2;
end;

:: deftheorem Def10 defines monic CAT_1:def 10 :
for b1 being Category
for b2 being Morphism of b1 holds
( b2 is monic iff for b3, b4 being Morphism of b1 st dom b3 = dom b4 & cod b3 = dom b2 & cod b4 = dom b2 & b2 * b3 = b2 * b4 holds
b3 = b4 );

definition
let c1 be Category;
let c2 be Morphism of c1;
attr a2 is epi means :: CAT_1:def 11
for b1, b2 being Morphism of a1 st dom b1 = cod a2 & dom b2 = cod a2 & cod b1 = cod b2 & b1 * a2 = b2 * a2 holds
b1 = b2;
end;

:: deftheorem Def11 defines epi CAT_1:def 11 :
for b1 being Category
for b2 being Morphism of b1 holds
( b2 is epi iff for b3, b4 being Morphism of b1 st dom b3 = cod b2 & dom b4 = cod b2 & cod b3 = cod b4 & b3 * b2 = b4 * b2 holds
b3 = b4 );

definition
let c1 be Category;
let c2 be Morphism of c1;
attr a2 is invertible means :: CAT_1:def 12
ex b1 being Morphism of a1 st
( dom b1 = cod a2 & cod b1 = dom a2 & a2 * b1 = id (cod a2) & b1 * a2 = id (dom a2) );
end;

:: deftheorem Def12 defines invertible CAT_1:def 12 :
for b1 being Category
for b2 being Morphism of b1 holds
( b2 is invertible iff ex b3 being Morphism of b1 st
( dom b3 = cod b2 & cod b3 = dom b2 & b2 * b3 = id (cod b2) & b3 * b2 = id (dom b2) ) );

theorem Th48: :: CAT_1:48
canceled;

theorem Th49: :: CAT_1:49
canceled;

theorem Th50: :: CAT_1:50
canceled;

theorem Th51: :: CAT_1:51
for b1 being Category
for b2, b3, b4 being Object of b1
for b5 being Morphism of b2,b3
for b6 being Morphism of b3,b4 st Hom b2,b3 <> {} & Hom b3,b4 <> {} holds
b6 * b5 in Hom b2,b4
proof end;

theorem Th52: :: CAT_1:52
for b1 being Category
for b2, b3, b4 being Object of b1 st Hom b2,b3 <> {} & Hom b3,b4 <> {} holds
Hom b2,b4 <> {} by Th51;

definition
let c1 be Category;
let c2, c3, c4 be Object of c1;
let c5 be Morphism of c2,c3;
let c6 be Morphism of c3,c4;
assume E26: ( Hom c2,c3 <> {} & Hom c3,c4 <> {} ) ;
func c6 * c5 -> Morphism of a2,a4 equals :Def13: :: CAT_1:def 13
a6 * a5;
correctness
coherence
c6 * c5 is Morphism of c2,c4;
proof end;
end;

:: deftheorem Def13 defines * CAT_1:def 13 :
for b1 being Category
for b2, b3, b4 being Object of b1
for b5 being Morphism of b2,b3
for b6 being Morphism of b3,b4 st Hom b2,b3 <> {} & Hom b3,b4 <> {} holds
b6 * b5 = b6 * b5;

theorem Th53: :: CAT_1:53
canceled;

theorem Th54: :: CAT_1:54
for b1 being Category
for b2, b3, b4, b5 being Object of b1
for b6 being Morphism of b2,b3
for b7 being Morphism of b3,b4
for b8 being Morphism of b4,b5 st Hom b2,b3 <> {} & Hom b3,b4 <> {} & Hom b4,b5 <> {} holds
(b8 * b7) * b6 = b8 * (b7 * b6)
proof end;

theorem Th55: :: CAT_1:55
for b1 being Category
for b2 being Object of b1 holds id b2 in Hom b2,b2
proof end;

theorem Th56: :: CAT_1:56
for b1 being Category
for b2 being Object of b1 holds Hom b2,b2 <> {} by Th55;

definition
let c1 be Category;
let c2 be Object of c1;
redefine func id as id c2 -> Morphism of a2,a2;
coherence
id c2 is Morphism of c2,c2
proof end;
end;

theorem Th57: :: CAT_1:57
for b1 being Category
for b2, b3 being Object of b1
for b4 being Morphism of b2,b3 st Hom b2,b3 <> {} holds
(id b3) * b4 = b4
proof end;

theorem Th58: :: CAT_1:58
for b1 being Category
for b2, b3 being Object of b1
for b4 being Morphism of b2,b3 st Hom b2,b3 <> {} holds
b4 * (id b2) = b4
proof end;

theorem Th59: :: CAT_1:59
for b1 being Category
for b2 being Object of b1 holds (id b2) * (id b2) = id b2
proof end;

theorem Th60: :: CAT_1:60
for b1 being Category
for b2, b3 being Object of b1
for b4 being Morphism of b2,b3 st Hom b2,b3 <> {} holds
( b4 is monic iff for b5 being Object of b1
for b6, b7 being Morphism of b5,b2 st Hom b5,b2 <> {} & b4 * b6 = b4 * b7 holds
b6 = b7 )
proof end;

theorem Th61: :: CAT_1:61
for b1 being Category
for b2, b3, b4 being Object of b1
for b5 being Morphism of b2,b3
for b6 being Morphism of b3,b4 st Hom b2,b3 <> {} & Hom b3,b4 <> {} & b5 is monic & b6 is monic holds
b6 * b5 is monic
proof end;

theorem Th62: :: CAT_1:62
for b1 being Category
for b2, b3, b4 being Object of b1
for b5 being Morphism of b2,b3
for b6 being Morphism of b3,b4 st Hom b2,b3 <> {} & Hom b3,b4 <> {} & b6 * b5 is monic holds
b5 is monic
proof end;

theorem Th63: :: CAT_1:63
for b1 being Category
for b2, b3 being Object of b1
for b4 being Morphism of b2,b3
for b5 being Morphism of b3,b2 st Hom b2,b3 <> {} & Hom b3,b2 <> {} & b4 * b5 = id b3 holds
b5 is monic
proof end;

theorem Th64: :: CAT_1:64
for b1 being Category
for b2 being Object of b1 holds id b2 is monic
proof end;

theorem Th65: :: CAT_1:65
for b1 being Category
for b2, b3 being Object of b1
for b4 being Morphism of b2,b3 st Hom b2,b3 <> {} holds
( b4 is epi iff for b5 being Object of b1
for b6, b7 being Morphism of b3,b5 st Hom b3,b5 <> {} & b6 * b4 = b7 * b4 holds
b6 = b7 )
proof end;

theorem Th66: :: CAT_1:66
for b1 being Category
for b2, b3, b4 being Object of b1
for b5 being Morphism of b2,b3
for b6 being Morphism of b3,b4 st Hom b2,b3 <> {} & Hom b3,b4 <> {} & b5 is epi & b6 is epi holds
b6 * b5 is epi
proof end;

theorem Th67: :: CAT_1:67
for b1 being Category
for b2, b3, b4 being Object of b1
for b5 being Morphism of b2,b3
for b6 being Morphism of b3,b4 st Hom b2,b3 <> {} & Hom b3,b4 <> {} & b6 * b5 is epi holds
b6 is epi
proof end;

theorem Th68: :: CAT_1:68
for b1 being Category
for b2, b3 being Object of b1
for b4 being Morphism of b2,b3
for b5 being Morphism of b3,b2 st Hom b2,b3 <> {} & Hom b3,b2 <> {} & b4 * b5 = id b3 holds
b4 is epi
proof end;

theorem Th69: :: CAT_1:69
for b1 being Category
for b2 being Object of b1 holds id b2 is epi
proof end;

theorem Th70: :: CAT_1:70
for b1 being Category
for b2, b3 being Object of b1
for b4 being Morphism of b2,b3 st Hom b2,b3 <> {} holds
( b4 is invertible iff ( Hom b3,b2 <> {} & ex b5 being Morphism of b3,b2 st
( b4 * b5 = id b3 & b5 * b4 = id b2 ) ) )
proof end;

theorem Th71: :: CAT_1:71
for b1 being Category
for b2, b3 being Object of b1
for b4 being Morphism of b2,b3 st Hom b2,b3 <> {} & Hom b3,b2 <> {} holds
for b5, b6 being Morphism of b3,b2 st b4 * b5 = id b3 & b6 * b4 = id b2 holds
b5 = b6
proof end;

definition
let c1 be Category;
let c2, c3 be Object of c1;
let c4 be Morphism of c2,c3;
assume that
E36: Hom c2,c3 <> {} and
E37: c4 is invertible ;
func c4 " -> Morphism of a3,a2 means :Def14: :: CAT_1:def 14
( a4 * a5 = id a3 & a5 * a4 = id a2 );
existence
ex b1 being Morphism of c3,c2 st
( c4 * b1 = id c3 & b1 * c4 = id c2 ) by E36, E37, Th70;
uniqueness
for b1, b2 being Morphism of c3,c2 st c4 * b1 = id c3 & b1 * c4 = id c2 & c4 * b2 = id c3 & b2 * c4 = id c2 holds
b1 = b2
proof end;
end;

:: deftheorem Def14 defines " CAT_1:def 14 :
for b1 being Category
for b2, b3 being Object of b1
for b4 being Morphism of b2,b3 st Hom b2,b3 <> {} & b4 is invertible holds
for b5 being Morphism of b3,b2 holds
( b5 = b4 " iff ( b4 * b5 = id b3 & b5 * b4 = id b2 ) );

theorem Th72: :: CAT_1:72
canceled;

theorem Th73: :: CAT_1:73
for b1 being Category
for b2, b3 being Object of b1
for b4 being Morphism of b2,b3 st Hom b2,b3 <> {} & b4 is invertible holds
( b4 is monic & b4 is epi )
proof end;

theorem Th74: :: CAT_1:74
for b1 being Category
for b2 being Object of b1 holds id b2 is invertible
proof end;

theorem Th75: :: CAT_1:75
for b1 being Category
for b2, b3, b4 being Object of b1
for b5 being Morphism of b2,b3
for b6 being Morphism of b3,b4 st Hom b2,b3 <> {} & Hom b3,b4 <> {} & b5 is invertible & b6 is invertible holds
b6 * b5 is invertible
proof end;

theorem Th76: :: CAT_1:76
for b1 being Category
for b2, b3 being Object of b1
for b4 being Morphism of b2,b3 st Hom b2,b3 <> {} & b4 is invertible holds
b4 " is invertible
proof end;

theorem Th77: :: CAT_1:77
for b1 being Category
for b2, b3, b4 being Object of b1
for b5 being Morphism of b2,b3
for b6 being Morphism of b3,b4 st Hom b2,b3 <> {} & Hom b3,b4 <> {} & b5 is invertible & b6 is invertible holds
(b6 * b5) " = (b5 " ) * (b6 " )
proof end;

definition
let c1 be Category;
let c2 be Object of c1;
attr a2 is terminal means :Def15: :: CAT_1:def 15
for b1 being Object of a1 holds
( Hom b1,a2 <> {} & ex b2 being Morphism of b1,a2 st
for b3 being Morphism of b1,a2 holds b2 = b3 );
attr a2 is initial means :Def16: :: CAT_1:def 16
for b1 being Object of a1 holds
( Hom a2,b1 <> {} & ex b2 being Morphism of a2,b1 st
for b3 being Morphism of a2,b1 holds b2 = b3 );
let c3 be Object of c1;
pred c2,c3 are_isomorphic means :Def17: :: CAT_1:def 17
( Hom a2,a3 <> {} & ex b1 being Morphism of a2,a3 st b1 is invertible );
end;

:: deftheorem Def15 defines terminal CAT_1:def 15 :
for b1 being Category
for b2 being Object of b1 holds
( b2 is terminal iff for b3 being Object of b1 holds
( Hom b3,b2 <> {} & ex b4 being Morphism of b3,b2 st
for b5 being Morphism of b3,b2 holds b4 = b5 ) );

:: deftheorem Def16 defines initial CAT_1:def 16 :
for b1 being Category
for b2 being Object of b1 holds
( b2 is initial iff for b3 being Object of b1 holds
( Hom b2,b3 <> {} & ex b4 being Morphism of b2,b3 st
for b5 being Morphism of b2,b3 holds b4 = b5 ) );

:: deftheorem Def17 defines are_isomorphic CAT_1:def 17 :
for b1 being Category
for b2, b3 being Object of b1 holds
( b2,b3 are_isomorphic iff ( Hom b2,b3 <> {} & ex b4 being Morphism of b2,b3 st b4 is invertible ) );

theorem Th78: :: CAT_1:78
canceled;

theorem Th79: :: CAT_1:79
canceled;

theorem Th80: :: CAT_1:80
canceled;

theorem Th81: :: CAT_1:81
for b1 being Category
for b2, b3 being Object of b1 holds
( b2,b3 are_isomorphic iff ( Hom b2,b3 <> {} & Hom b3,b2 <> {} & ex b4 being Morphism of b2,b3ex b5 being Morphism of b3,b2 st
( b4 * b5 = id b3 & b5 * b4 = id b2 ) ) )
proof end;

theorem Th82: :: CAT_1:82
for b1 being Category
for b2 being Object of b1 holds
( b2 is initial iff for b3 being Object of b1 ex b4 being Morphism of b2,b3 st Hom b2,b3 = {b4} )
proof end;

theorem Th83: :: CAT_1:83
for b1 being Category
for b2 being Object of b1 st b2 is initial holds
for b3 being Morphism of b2,b2 holds id b2 = b3
proof end;

theorem Th84: :: CAT_1:84
for b1 being Category
for b2, b3 being Object of b1 st b2 is initial & b3 is initial holds
b2,b3 are_isomorphic
proof end;

theorem Th85: :: CAT_1:85
for b1 being Category
for b2, b3 being Object of b1 st b2 is initial & b2,b3 are_isomorphic holds
b3 is initial
proof end;

theorem Th86: :: CAT_1:86
for b1 being Category
for b2 being Object of b1 holds
( b2 is terminal iff for b3 being Object of b1 ex b4 being Morphism of b3,b2 st Hom b3,b2 = {b4} )
proof end;

theorem Th87: :: CAT_1:87
for b1 being Category
for b2 being Object of b1 st b2 is terminal holds
for b3 being Morphism of b2,b2 holds id b2 = b3
proof end;

theorem Th88: :: CAT_1:88
for b1 being Category
for b2, b3 being Object of b1 st b2 is terminal & b3 is terminal holds
b2,b3 are_isomorphic
proof end;

theorem Th89: :: CAT_1:89
for b1 being Category
for b2, b3 being Object of b1 st b2 is terminal & b3,b2 are_isomorphic holds
b3 is terminal
proof end;

theorem Th90: :: CAT_1:90
for b1 being Category
for b2, b3 being Object of b1
for b4 being Morphism of b2,b3 st Hom b2,b3 <> {} & b2 is terminal holds
b4 is monic
proof end;

theorem Th91: :: CAT_1:91
for b1 being Category
for b2 being Object of b1 holds b2,b2 are_isomorphic
proof end;

theorem Th92: :: CAT_1:92
for b1 being Category
for b2, b3 being Object of b1 st b2,b3 are_isomorphic holds
b3,b2 are_isomorphic
proof end;

theorem Th93: :: CAT_1:93
for b1 being Category
for b2, b3, b4 being Object of b1 st b2,b3 are_isomorphic & b3,b4 are_isomorphic holds
b2,b4 are_isomorphic
proof end;

definition
let c1, c2 be Category;
mode Functor of c1,c2 -> Function of the Morphisms of a1,the Morphisms of a2 means :Def18: :: CAT_1:def 18
( ( for b1 being Element of the Objects of a1 ex b2 being Element of the Objects of a2 st a3 . (the Id of a1 . b1) = the Id of a2 . b2 ) & ( for b1 being Element of the Morphisms of a1 holds
( a3 . (the Id of a1 . (the Dom of a1 . b1)) = the Id of a2 . (the Dom of a2 . (a3 . b1)) & a3 . (the Id of a1 . (the Cod of a1 . b1)) = the Id of a2 . (the Cod of a2 . (a3 . b1)) ) ) & ( for b1, b2 being Element of the Morphisms of a1 st [b2,b1] in dom the Comp of a1 holds
a3 . (the Comp of a1 . [b2,b1]) = the Comp of a2 . [(a3 . b2),(a3 . b1)] ) );
existence
ex b1 being Function of the Morphisms of c1,the Morphisms of c2 st
( ( for b2 being Element of the Objects of c1 ex b3 being Element of the Objects of c2 st b1 . (the Id of c1 . b2) = the Id of c2 . b3 ) & ( for b2 being Element of the Morphisms of c1 holds
( b1 . (the Id of c1 . (the Dom of c1 . b2)) = the Id of c2 . (the Dom of c2 . (b1 . b2)) & b1 . (the Id of c1 . (the Cod of c1 . b2)) = the Id of c2 . (the Cod of c2 . (b1 . b2)) ) ) & ( for b2, b3 being Element of the Morphisms of c1 st [b3,b2] in dom the Comp of c1 holds
b1 . (the Comp of c1 . [b3,b2]) = the Comp of c2 . [(b1 . b3),(b1 . b2)] ) )
proof end;
end;

:: deftheorem Def18 defines Functor CAT_1:def 18 :
for b1, b2 being Category
for b3 being Function of the Morphisms of b1,the Morphisms of b2 holds
( b3 is Functor of b1,b2 iff ( ( for b4 being Element of the Objects of b1 ex b5 being Element of the Objects of b2 st b3 . (the Id of b1 . b4) = the Id of b2 . b5 ) & ( for b4 being Element of the Morphisms of b1 holds
( b3 . (the Id of b1 . (the Dom of b1 . b4)) = the Id of b2 . (the Dom of b2 . (b3 . b4)) & b3 . (the Id of b1 . (the Cod of b1 . b4)) = the Id of b2 . (the Cod of b2 . (b3 . b4)) ) ) & ( for b4, b5 being Element of the Morphisms of b1 st [b5,b4] in dom the Comp of b1 holds
b3 . (the Comp of b1 . [b5,b4]) = the Comp of b2 . [(b3 . b5),(b3 . b4)] ) ) );

theorem Th94: :: CAT_1:94
canceled;

theorem Th95: :: CAT_1:95
canceled;

theorem Th96: :: CAT_1:96
for b1, b2 being Category
for b3 being Function of the Morphisms of b1,the Morphisms of b2 st ( for b4 being Object of b1 ex b5 being Object of b2 st b3 . (id b4) = id b5 ) & ( for b4 being Morphism of b1 holds
( b3 . (id (dom b4)) = id (dom (b3 . b4)) & b3 . (id (cod b4)) = id (cod (b3 . b4)) ) ) & ( for b4, b5 being Morphism of b1 st dom b5 = cod b4 holds
b3 . (b5 * b4) = (b3 . b5) * (b3 . b4) ) holds
b3 is Functor of b1,b2
proof end;

theorem Th97: :: CAT_1:97
for b1, b2 being Category
for b3 being Functor of b1,b2
for b4 being Object of b1 ex b5 being Object of b2 st b3 . (id b4) = id b5
proof end;

theorem Th98: :: CAT_1:98
for b1, b2 being Category
for b3 being Functor of b1,b2
for b4 being Morphism of b1 holds
( b3 . (id (dom b4)) = id (dom (b3 . b4)) & b3 . (id (cod b4)) = id (cod (b3 . b4)) ) by Def18;

theorem Th99: :: CAT_1:99
for b1, b2 being Category
for b3 being Functor of b1,b2
for b4, b5 being Morphism of b1 st dom b5 = cod b4 holds
( dom (b3 . b5) = cod (b3 . b4) & b3 . (b5 * b4) = (b3 . b5) * (b3 . b4) )
proof end;

theorem Th100: :: CAT_1:100
for b1, b2 being Category
for b3 being Function of the Morphisms of b1,the Morphisms of b2
for b4 being Function of the Objects of b1,the Objects of b2 st ( for b5 being Object of b1 holds b3 . (id b5) = id (b4 . b5) ) & ( for b5 being Morphism of b1 holds
( b4 . (dom b5) = dom (b3 . b5) & b4 . (cod b5) = cod (b3 . b5) ) ) & ( for b5, b6 being Morphism of b1 st dom b6 = cod b5 holds
b3 . (b6 * b5) = (b3 . b6) * (b3 . b5) ) holds
b3 is Functor of b1,b2
proof end;

definition
let c1, c2 be Category;
let c3 be Function of the Morphisms of c1,the Morphisms of c2;
assume E50: for b1 being Element of the Objects of c1 ex b2 being Element of the Objects of c2 st c3 . (the Id of c1 . b1) = the Id of c2 . b2 ;
func Obj c3 -> Function of the Objects of a1,the Objects of a2 means :Def19: :: CAT_1:def 19
for b1 being Element of the Objects of a1
for b2 being Element of the Objects of a2 st a3 . (the Id of a1 . b1) = the Id of a2 . b2 holds
a4 . b1 = b2;
existence
ex b1 being Function of the Objects of c1,the Objects of c2 st
for b2 being Element of the Objects of c1
for b3 being Element of the Objects of c2 st c3 . (the Id of c1 . b2) = the Id of c2 . b3 holds
b1 . b2 = b3
proof end;
uniqueness
for b1, b2 being Function of the Objects of c1,the Objects of c2 st ( for b3 being Element of the Objects of c1
for b4 being Element of the Objects of c2 st c3 . (the Id of c1 . b3) = the Id of c2 . b4 holds
b1 . b3 = b4 ) & ( for b3 being Element of the Objects of c1
for b4 being Element of the Objects of c2 st c3 . (the Id of c1 . b3) = the Id of c2 . b4 holds
b2 . b3 = b4 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def19 defines Obj CAT_1:def 19 :
for b1, b2 being Category
for b3 being Function of the Morphisms of b1,the Morphisms of b2 st ( for b4 being Element of the Objects of b1 ex b5 being Element of the Objects of b2 st b3 . (the Id of b1 . b4) = the Id of b2 . b5 ) holds
for b4 being Function of the Objects of b1,the Objects of b2 holds
( b4 = Obj b3 iff for b5 being Element of the Objects of b1
for b6 being Element of the Objects of b2 st b3 . (the Id of b1 . b5) = the Id of b2 . b6 holds
b4 . b5 = b6 );

theorem Th101: :: CAT_1:101
canceled;

theorem Th102: :: CAT_1:102
for b1, b2 being Category
for b3 being Function of the Morphisms of b1,the Morphisms of b2 st ( for b4 being Object of b1 ex b5 being Object of b2 st b3 . (id b4) = id b5 ) holds
for b4 being Object of b1
for b5 being Object of b2 st b3 . (id b4) = id b5 holds
(Obj b3) . b4 = b5
proof end;

theorem Th103: :: CAT_1:103
for b1, b2 being Category
for b3 being Functor of b1,b2
for b4 being Object of b1
for b5 being Object of b2 st b3 . (id b4) = id b5 holds
(Obj b3) . b4 = b5
proof end;

theorem Th104: :: CAT_1:104
for b1, b2 being Category
for b3 being Functor of b1,b2
for b4 being Object of b1 holds b3 . (id b4) = id ((Obj b3) . b4)
proof end;

theorem Th105: :: CAT_1:105
for b1, b2 being Category
for b3 being Functor of b1,b2
for b4 being Morphism of b1 holds
( (Obj b3) . (dom b4) = dom (b3 . b4) & (Obj b3) . (cod b4) = cod (b3 . b4) )
proof end;

definition
let c1, c2 be Category;
let c3 be Functor of c1,c2;
let c4 be Object of c1;
func c3 . c4 -> Object of a2 equals :: CAT_1:def 20
(Obj a3) . a4;
correctness
coherence
(Obj c3) . c4 is Object of c2;
;
end;

:: deftheorem Def20 defines . CAT_1:def 20 :
for b1, b2 being Category
for b3 being Functor of b1,b2
for b4 being Object of b1 holds b3 . b4 = (Obj b3) . b4;

theorem Th106: :: CAT_1:106
canceled;

theorem Th107: :: CAT_1:107
for b1, b2 being Category
for b3 being Functor of b1,b2
for b4 being Object of b1
for b5 being Object of b2 st b3 . (id b4) = id b5 holds
b3 . b4 = b5 by Th103;

theorem Th108: :: CAT_1:108
for b1, b2 being Category
for b3 being Functor of b1,b2
for b4 being Object of b1 holds b3 . (id b4) = id (b3 . b4) by Th104;

theorem Th109: :: CAT_1:109
for b1, b2 being Category
for b3 being Functor of b1,b2
for b4 being Morphism of b1 holds
( b3 . (dom b4) = dom (b3 . b4) & b3 . (cod b4) = cod (b3 . b4) ) by Th105;

theorem Th110: :: CAT_1:110
for b1, b2, b3 being Category
for b4 being Functor of b1,b2
for b5 being Functor of b2,b3 holds b5 * b4 is Functor of b1,b3
proof end;

definition
let c1, c2, c3 be Category;
let c4 be Functor of c1,c2;
let c5 be Functor of c2,c3;
redefine func * as c5 * c4 -> Functor of a1,a3;
coherence
c4 * c5 is Functor of c1,c3 by Th110;
end;

theorem Th111: :: CAT_1:111
for b1 being Category holds id the Morphisms of b1 is Functor of b1,b1
proof end;

theorem Th112: :: CAT_1:112
for b1, b2, b3 being Category
for b4 being Functor of b1,b2
for b5 being Functor of b2,b3
for b6 being Object of b1 holds (Obj (b5 * b4)) . b6 = (Obj b5) . ((Obj b4) . b6)
proof end;

theorem Th113: :: CAT_1:113
for b1, b2, b3 being Category
for b4 being Functor of b1,b2
for b5 being Functor of b2,b3
for b6 being Object of b1 holds (b5 * b4) . b6 = b5 . (b4 . b6) by Th112;

definition
let c1 be Category;
func id c1 -> Functor of a1,a1 equals :: CAT_1:def 21
 id the Morphisms of a1;
coherence
id the Morphisms of c1 is Functor of c1,c1 by Th111;
end;

:: deftheorem Def21 defines id CAT_1:def 21 :
for b1 being Category holds id b1 = id the Morphisms of b1;

theorem Th114: :: CAT_1:114
canceled;

theorem Th115: :: CAT_1:115
for b1 being Category
for b2 being Morphism of b1 holds (id b1) . b2 = b2 by FUNCT_1:35;

theorem Th116: :: CAT_1:116
for b1 being Category
for b2 being Object of b1 holds (Obj (id b1)) . b2 = b2
proof end;

theorem Th117: :: CAT_1:117
for b1 being Category holds Obj (id b1) = id the Objects of b1
proof end;

theorem Th118: :: CAT_1:118
for b1 being Category
for b2 being Object of b1 holds (id b1) . b2 = b2 by Th116;

definition
let c1, c2 be Category;
let c3 be Functor of c1,c2;
attr a3 is isomorphic means :: CAT_1:def 22
( a3 is one-to-one & rng a3 = the Morphisms of a2 & rng (Obj a3) = the Objects of a2 );
attr a3 is full means :Def23: :: CAT_1:def 23
for b1, b2 being Object of a1 st Hom (a3 . b1),(a3 . b2) <> {} holds
for b3 being Morphism of a3 . b1,a3 . b2 holds
( Hom b1,b2 <> {} & ex b4 being Morphism of b1,b2 st b3 = a3 . b4 );
attr a3 is faithful means :Def24: :: CAT_1:def 24
for b1, b2 being Object of a1 st Hom b1,b2 <> {} holds
for b3, b4 being Morphism of b1,b2 st a3 . b3 = a3 . b4 holds
b3 = b4;
end;

:: deftheorem Def22 defines isomorphic CAT_1:def 22 :
for b1, b2 being Category
for b3 being Functor of b1,b2 holds
( b3 is isomorphic iff ( b3 is one-to-one & rng b3 = the Morphisms of b2 & rng (Obj b3) = the Objects of b2 ) );

:: deftheorem Def23 defines full CAT_1:def 23 :
for b1, b2 being Category
for b3 being Functor of b1,b2 holds
( b3 is full iff for b4, b5 being Object of b1 st Hom (b3 . b4),(b3 . b5) <> {} holds
for b6 being Morphism of b3 . b4,b3 . b5 holds
( Hom b4,b5 <> {} & ex b7 being Morphism of b4,b5 st b6 = b3 . b7 ) );

:: deftheorem Def24 defines faithful CAT_1:def 24 :
for b1, b2 being Category
for b3 being Functor of b1,b2 holds
( b3 is faithful iff for b4, b5 being Object of b1 st Hom b4,b5 <> {} holds
for b6, b7 being Morphism of b4,b5 st b3 . b6 = b3 . b7 holds
b6 = b7 );

notation
let c1, c2 be Category;
let c3 be Functor of c1,c2;
synonym c3 is_an_isomorphism for isomorphic c3;
end;

theorem Th119: :: CAT_1:119
canceled;

theorem Th120: :: CAT_1:120
canceled;

theorem Th121: :: CAT_1:121
canceled;

theorem Th122: :: CAT_1:122
for b1 being Category holds id b1 is_an_isomorphism
proof end;

theorem Th123: :: CAT_1:123
for b1, b2 being Category
for b3 being Functor of b1,b2
for b4, b5 being Object of b1
for b6 being set st b6 in Hom b4,b5 holds
b3 . b6 in Hom (b3 . b4),(b3 . b5)
proof end;

theorem Th124: :: CAT_1:124
for b1, b2 being Category
for b3 being Functor of b1,b2
for b4, b5 being Object of b1 st Hom b4,b5 <> {} holds
for b6 being Morphism of b4,b5 holds b3 . b6 in Hom (b3 . b4),(b3 . b5)
proof end;

theorem Th125: :: CAT_1:125
for b1, b2 being Category
for b3 being Functor of b1,b2
for b4, b5 being Object of b1 st Hom b4,b5 <> {} holds
for b6 being Morphism of b4,b5 holds b3 . b6 is Morphism of b3 . b4,b3 . b5
proof end;

theorem Th126: :: CAT_1:126
for b1, b2 being Category
for b3 being Functor of b1,b2
for b4, b5 being Object of b1 st Hom b4,b5 <> {} holds
Hom (b3 . b4),(b3 . b5) <> {}
proof end;

theorem Th127: :: CAT_1:127
for b1, b2, b3 being Category
for b4 being Functor of b1,b2
for b5 being Functor of b2,b3 st b4 is full & b5 is full holds
b5 * b4 is full
proof end;

theorem Th128: :: CAT_1:128
for b1, b2, b3 being Category
for b4 being Functor of b1,b2
for b5 being Functor of b2,b3 st b4 is faithful & b5 is faithful holds
b5 * b4 is faithful
proof end;

theorem Th129: :: CAT_1:129
for b1, b2 being Category
for b3 being Functor of b1,b2
for b4, b5 being Object of b1 holds b3 .: (Hom b4,b5) c= Hom (b3 . b4),(b3 . b5)
proof end;

definition
let c1, c2 be Category;
let c3 be Functor of c1,c2;
let c4, c5 be Object of c1;
func hom c3,c4,c5 -> Function of Hom a4,a5, Hom (a3 . a4),(a3 . a5) equals :: CAT_1:def 25
a3 | (Hom a4,a5);
correctness
coherence
c3 | (Hom c4,c5) is Function of Hom c4,c5, Hom (c3 . c4),(c3 . c5);
proof end;
end;

:: deftheorem Def25 defines hom CAT_1:def 25 :
for b1, b2 being Category
for b3 being Functor of b1,b2
for b4, b5 being Object of b1 holds hom b3,b4,b5 = b3 | (Hom b4,b5);

theorem Th130: :: CAT_1:130
canceled;

theorem Th131: :: CAT_1:131
for b1, b2 being Category
for b3 being Functor of b1,b2
for b4, b5 being Object of b1 st Hom b4,b5 <> {} holds
for b6 being Morphism of b4,b5 holds (hom b3,b4,b5) . b6 = b3 . b6
proof end;

theorem Th132: :: CAT_1:132
for b1, b2 being Category
for b3 being Functor of b1,b2 holds
( b3 is full iff for b4, b5 being Object of b1 holds rng (hom b3,b4,b5) = Hom (b3 . b4),(b3 . b5) )
proof end;

theorem Th133: :: CAT_1:133
for b1, b2 being Category
for b3 being Functor of b1,b2 holds
( b3 is faithful iff for b4, b5 being Object of b1 holds hom b3,b4,b5 is one-to-one )
proof end;