:: Examples of Category Structures.Subcategories
:: by Andrzej Trybulec
::
:: Received January 22, 1996
:: Copyright (c) 1996-2012 Association of Mizar Users


begin

theorem :: ALTCAT_2:1
for X1, X2, a1, a2 being set holds [:(X1 --> a1),(X2 --> a2):] = [:X1,X2:] --> [a1,a2]
proofend;

registration
let I be set ;
cluster [[0]] I ->  Function-yielding ;
coherence
 [[0]] I is Function-yielding ;
end;

theorem :: ALTCAT_2:2
for f, g being Function holds ~ (g * f) = g * (~ f)
proofend;

theorem :: ALTCAT_2:3
for f, g, h being Function holds ~ (f * [:g,h:]) = (~ f) * [:h,g:]
proofend;

registration
let f be Function-yielding Function;
cluster ~ f ->  Function-yielding ;
coherence
 ~ f is Function-yielding
proofend;
end;

theorem :: ALTCAT_2:4
for I being set
for A, B, C being ManySortedSet of I st A is_transformable_to B holds
for F being ManySortedFunction of A,B
for G being ManySortedFunction of B,C holds G ** F is ManySortedFunction of A,C
proofend;

registration
let I be set ;
let A be ManySortedSet of [:I,I:];
cluster ~ A -> [:I,I:] -defined ;
coherence
 ~ A is [:I,I:] -defined ;
end;

registration
let I be set ;
let A be ManySortedSet of [:I,I:];
cluster ~ A -> [:I,I:] -defined total for [:I,I:] -defined Function;
coherence
 for b1 being [:I,I:] -defined Function st b1 = ~ A holds
b1 is total ;
end;

theorem :: ALTCAT_2:5
for I1 being set
for I2 being non empty set
for f being Function of I1,I2
for B, C being ManySortedSet of I2
for G being ManySortedFunction of B,C holds G * f is ManySortedFunction of B * f,C * f
proofend;

definition
let I be set ;
let A, B be ManySortedSet of [:I,I:];
let F be ManySortedFunction of A,B;
:: original:~
redefine func ~ F ->  ManySortedFunction of ~ A, ~ B;
coherence
 ~ F is ManySortedFunction of ~ A, ~ B
proofend;
end;

theorem :: ALTCAT_2:6
for I1, I2 being non empty set
for M being ManySortedSet of [:I1,I2:]
for o1 being Element of I1
for o2 being Element of I2 holds (~ M) . (o2,o1) = M . (o1,o2)
proofend;

registration
let I1 be set ;
let f, g be ManySortedFunction of I1;
clusterg ** f -> I1 -defined ;
coherence
 g ** f is I1 -defined
proofend;
end;

registration
let I1 be set ;
let f, g be ManySortedFunction of I1;
clusterg ** f ->  total ;
coherence
 g ** f is total
proofend;
end;

begin

definition
let f, g be Function;
predf cc= g means :Def1: :: ALTCAT_2:def 1
( dom f c= dom g & ( for i being set st i in dom f holds
f . i c= g . i ) );
reflexivity
 for f being Function holds
( dom f c= dom f & ( for i being set st i in dom f holds
f . i c= f . i ) ) ;
end;

:: deftheorem Def1 defines cc= ALTCAT_2:def_1_:_
 for f, g being Function holds
( f cc= g iff ( dom f c= dom g & ( for i being set st i in dom f holds
f . i c= g . i ) ) );

definition
let I, J be set ;
let A be ManySortedSet of I;
let B be ManySortedSet of J;
:: original:cc=
redefine predA cc= B means :Def2: :: ALTCAT_2:def 2
( I c= J & ( for i being set st i in I holds
A . i c= B . i ) );
compatibility
 ( A cc= B iff ( I c= J & ( for i being set st i in I holds
A . i c= B . i ) ) )
proofend;
end;

:: deftheorem Def2 defines cc= ALTCAT_2:def_2_:_
 for I, J being set
for A being ManySortedSet of I
for B being ManySortedSet of J holds
( A cc= B iff ( I c= J & ( for i being set st i in I holds
A . i c= B . i ) ) );

theorem Th7: :: ALTCAT_2:7
for I, J being set
for A being ManySortedSet of I
for B being ManySortedSet of J st A cc= B & B cc= A holds
A = B
proofend;

theorem Th8: :: ALTCAT_2:8
for I, J, K being set
for A being ManySortedSet of I
for B being ManySortedSet of J
for C being ManySortedSet of K st A cc= B & B cc= C holds
A cc= C
proofend;

theorem :: ALTCAT_2:9
for I being set
for A, B being ManySortedSet of I holds
( A cc= B iff A c= B )
proofend;

begin

scheme :: ALTCAT_2:sch 1
OnSingletons{ F1() ->  non empty set , F2( set ) ->  set , P1[ set ] } :
  {  [o,F2(o)] where o is Element of F1() : P1[o]  }  is Function
proofend;

scheme :: ALTCAT_2:sch 2
DomOnSingletons{ F1() ->  non empty set , F2() ->  Function, F3( set ) ->  set , P1[ set ] } :
 dom F2() =  {  o where o is Element of F1() : P1[o]  }
provided
A1: F2() =  {  [o,F3(o)] where o is Element of F1() : P1[o]  }
proofend;

scheme :: ALTCAT_2:sch 3
ValOnSingletons{ F1() ->  non empty set , F2() ->  Function, F3() ->  Element of F1(), F4( set ) ->  set , P1[ set ] } :
 F2() . F3() = F4(F3())
provided
A1: F2() =  {  [o,F4(o)] where o is Element of F1() : P1[o]  }  and
A2: P1[F3()]
proofend;

begin

theorem Th10: :: ALTCAT_2:10
for C being Category
for i, j, k being Object of C holds [:(Hom (j,k)),(Hom (i,j)):] c= dom the Comp of C
proofend;

theorem Th11: :: ALTCAT_2:11
for C being Category
for i, j, k being Object of C holds the Comp of C .: [:(Hom (j,k)),(Hom (i,j)):] c= Hom (i,k)
proofend;

definition
let C be non empty non void CatStr ;
func the_hom_sets_of C ->  ManySortedSet of [: the carrier of C, the carrier of C:] means :Def3: :: ALTCAT_2:def 3
 for i, j being Object of C holds it . (i,j) = Hom (i,j);
existence
 ex b1 being ManySortedSet of [: the carrier of C, the carrier of C:] st
for i, j being Object of C holds b1 . (i,j) = Hom (i,j)
proofend;
uniqueness
 for b1, b2 being ManySortedSet of [: the carrier of C, the carrier of C:] st ( for i, j being Object of C holds b1 . (i,j) = Hom (i,j) ) & ( for i, j being Object of C holds b2 . (i,j) = Hom (i,j) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def3 defines the_hom_sets_of ALTCAT_2:def_3_:_
 for C being non empty non void CatStr
for b2 being ManySortedSet of [: the carrier of C, the carrier of C:] holds
( b2 = the_hom_sets_of C iff for i, j being Object of C holds b2 . (i,j) = Hom (i,j) );

theorem Th12: :: ALTCAT_2:12
for C being Category
for i being Object of C holds id i in (the_hom_sets_of C) . (i,i)
proofend;

definition
let C be Category;
func the_comps_of C ->  BinComp of (the_hom_sets_of C) means :Def4: :: ALTCAT_2:def 4
 for i, j, k being Object of C holds it . (i,j,k) = the Comp of C | [:((the_hom_sets_of C) . (j,k)),((the_hom_sets_of C) . (i,j)):];
existence
 ex b1 being BinComp of (the_hom_sets_of C) st
for i, j, k being Object of C holds b1 . (i,j,k) = the Comp of C | [:((the_hom_sets_of C) . (j,k)),((the_hom_sets_of C) . (i,j)):]
proofend;
uniqueness
 for b1, b2 being BinComp of (the_hom_sets_of C) st ( for i, j, k being Object of C holds b1 . (i,j,k) = the Comp of C | [:((the_hom_sets_of C) . (j,k)),((the_hom_sets_of C) . (i,j)):] ) & ( for i, j, k being Object of C holds b2 . (i,j,k) = the Comp of C | [:((the_hom_sets_of C) . (j,k)),((the_hom_sets_of C) . (i,j)):] ) holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines the_comps_of ALTCAT_2:def_4_:_
 for C being Category
for b2 being BinComp of (the_hom_sets_of C) holds
( b2 = the_comps_of C iff for i, j, k being Object of C holds b2 . (i,j,k) = the Comp of C | [:((the_hom_sets_of C) . (j,k)),((the_hom_sets_of C) . (i,j)):] );

theorem Th13: :: ALTCAT_2:13
for C being Category
for i, j, k being Object of C st Hom (i,j) <> {} &amp; Hom (j,k) <> {} holds
for f being Morphism of i,j
for g being Morphism of j,k holds ((the_comps_of C) . (i,j,k)) . (g,f) = g * f
proofend;

theorem Th14: :: ALTCAT_2:14
for C being Category holds the_comps_of C is associative
proofend;

theorem Th15: :: ALTCAT_2:15
for C being Category holds
( the_comps_of C is with_left_units &amp; the_comps_of C is with_right_units )
proofend;

begin

definition
let C be Category;
func Alter C ->  non empty strict AltCatStr  equals :: ALTCAT_2:def 5
 AltCatStr(# the carrier of C,(the_hom_sets_of C),(the_comps_of C) #);
correctness
coherence
AltCatStr(# the carrier of C,(the_hom_sets_of C),(the_comps_of C) #) is non empty strict AltCatStr ;
;
end;

:: deftheorem  defines Alter ALTCAT_2:def_5_:_
 for C being Category holds Alter C = AltCatStr(# the carrier of C,(the_hom_sets_of C),(the_comps_of C) #);

theorem Th16: :: ALTCAT_2:16
for C being Category holds Alter C is associative
proofend;

theorem Th17: :: ALTCAT_2:17
for C being Category holds Alter C is with_units
proofend;

theorem Th18: :: ALTCAT_2:18
for C being Category holds Alter C is transitive
proofend;

registration
let C be Category;
cluster Alter C ->  non empty transitive strict associative with_units ;
coherence
 ( Alter C is transitive &amp; Alter C is associative &amp; Alter C is with_units ) by Th16, Th17, Th18;
end;

begin

registration
cluster non empty strict for AltGraph ;
existence
 ex b1 being AltGraph st
( not b1 is empty &amp; b1 is strict )
proofend;
end;

definition
let C be AltGraph ;
attrC is reflexive  means :Def6: :: ALTCAT_2:def 6
 for x being set st x in the carrier of C holds
the Arrows of C . (x,x) <> {} ;
end;

:: deftheorem Def6 defines reflexive ALTCAT_2:def_6_:_
 for C being AltGraph holds
( C is reflexive iff for x being set st x in the carrier of C holds
the Arrows of C . (x,x) <> {} );

definition
let C be non empty AltGraph ;
redefine attr C is reflexive  means :: ALTCAT_2:def 7
 for o being object of C holds <^o,o^> <> {} ;
compatibility
 ( C is reflexive iff for o being object of C holds <^o,o^> <> {} )
proofend;
end;

:: deftheorem  defines reflexive ALTCAT_2:def_7_:_
 for C being non empty AltGraph holds
( C is reflexive iff for o being object of C holds <^o,o^> <> {} );

definition
let C be non empty transitive AltCatStr ;
redefine attr C is associative  means :Def8: :: ALTCAT_2:def 8
 for o1, o2, o3, o4 being object of C
for f being Morphism of o1,o2
for g being Morphism of o2,o3
for h being Morphism of o3,o4 st <^o1,o2^> <> {} &amp; <^o2,o3^> <> {} &amp; <^o3,o4^> <> {} holds
(h * g) * f = h * (g * f);
compatibility
 ( C is associative iff for o1, o2, o3, o4 being object of C
for f being Morphism of o1,o2
for g being Morphism of o2,o3
for h being Morphism of o3,o4 st <^o1,o2^> <> {} &amp; <^o2,o3^> <> {} &amp; <^o3,o4^> <> {} holds
(h * g) * f = h * (g * f) )
proofend;
end;

:: deftheorem Def8 defines associative ALTCAT_2:def_8_:_
 for C being non empty transitive AltCatStr holds
( C is associative iff for o1, o2, o3, o4 being object of C
for f being Morphism of o1,o2
for g being Morphism of o2,o3
for h being Morphism of o3,o4 st <^o1,o2^> <> {} &amp; <^o2,o3^> <> {} &amp; <^o3,o4^> <> {} holds
(h * g) * f = h * (g * f) );

definition
let C be non empty AltCatStr ;
redefine attr C is with_units  means :: ALTCAT_2:def 9
 for o being object of C holds
( <^o,o^> <> {} &amp; ex i being Morphism of o,o st
for o9 being object of C
for m9 being Morphism of o9,o
for m99 being Morphism of o,o9 holds
( ( <^o9,o^> <> {} implies i * m9 = m9 ) &amp; ( <^o,o9^> <> {} implies m99 * i = m99 ) ) );
compatibility
 ( C is with_units iff for o being object of C holds
( <^o,o^> <> {} &amp; ex i being Morphism of o,o st
for o9 being object of C
for m9 being Morphism of o9,o
for m99 being Morphism of o,o9 holds
( ( <^o9,o^> <> {} implies i * m9 = m9 ) &amp; ( <^o,o9^> <> {} implies m99 * i = m99 ) ) ) )
proofend;
end;

:: deftheorem  defines with_units ALTCAT_2:def_9_:_
 for C being non empty AltCatStr holds
( C is with_units iff for o being object of C holds
( <^o,o^> <> {} &amp; ex i being Morphism of o,o st
for o9 being object of C
for m9 being Morphism of o9,o
for m99 being Morphism of o,o9 holds
( ( <^o9,o^> <> {} implies i * m9 = m9 ) &amp; ( <^o,o9^> <> {} implies m99 * i = m99 ) ) ) );

registration
cluster non empty with_units  ->  non empty reflexive for AltCatStr ;
coherence
 for b1 being non empty AltCatStr st b1 is with_units holds
b1 is reflexive
proofend;
end;

registration
cluster non empty reflexive for AltGraph ;
existence
 ex b1 being AltGraph st
( not b1 is empty &amp; b1 is reflexive )
proofend;
end;

registration
cluster non empty reflexive for AltCatStr ;
existence
 ex b1 being AltCatStr st
( not b1 is empty &amp; b1 is reflexive )
proofend;
end;

begin

Lm1:  for E1, E2 being strict AltCatStr st the carrier of E1 is empty &amp; the carrier of E2 is empty holds
E1 = E2
proofend;

definition
func the_empty_category  ->  strict AltCatStr  means :Def10: :: ALTCAT_2:def 10
 the carrier of it is empty ;
existence
 ex b1 being strict AltCatStr st the carrier of b1 is empty
proofend;
uniqueness
 for b1, b2 being strict AltCatStr st the carrier of b1 is empty &amp; the carrier of b2 is empty holds
b1 = b2 by Lm1;
end;

:: deftheorem Def10 defines the_empty_category ALTCAT_2:def_10_:_
 for b1 being strict AltCatStr holds
( b1 = the_empty_category iff the carrier of b1 is empty );

registration
cluster the_empty_category  ->  empty strict ;
coherence
 the_empty_category is empty by Def10;
end;

registration
cluster empty strict for AltCatStr ;
existence
 ex b1 being AltCatStr st
( b1 is empty &amp; b1 is strict )
proofend;
end;

theorem :: ALTCAT_2:19
for E being empty strict AltCatStr holds E = the_empty_category by Lm1;

begin

:: Semadeni Wiweger 1.6.1 str. 24
definition
let C be AltCatStr ;
mode SubCatStr of C ->  AltCatStr  means :Def11: :: ALTCAT_2:def 11
( the carrier of it c= the carrier of C &amp; the Arrows of it cc= the Arrows of C &amp; the Comp of it cc= the Comp of C );
existence
 ex b1 being AltCatStr st
( the carrier of b1 c= the carrier of C &amp; the Arrows of b1 cc= the Arrows of C &amp; the Comp of b1 cc= the Comp of C ) ;
end;

:: deftheorem Def11 defines SubCatStr ALTCAT_2:def_11_:_
 for C, b2 being AltCatStr holds
( b2 is SubCatStr of C iff ( the carrier of b2 c= the carrier of C &amp; the Arrows of b2 cc= the Arrows of C &amp; the Comp of b2 cc= the Comp of C ) );

theorem Th20: :: ALTCAT_2:20
for C being AltCatStr holds C is SubCatStr of C
proofend;

theorem :: ALTCAT_2:21
for C1, C2, C3 being AltCatStr st C1 is SubCatStr of C2 &amp; C2 is SubCatStr of C3 holds
C1 is SubCatStr of C3
proofend;

theorem Th22: :: ALTCAT_2:22
for C1, C2 being AltCatStr st C1 is SubCatStr of C2 &amp; C2 is SubCatStr of C1 holds
AltCatStr(# the carrier of C1, the Arrows of C1, the Comp of C1 #) = AltCatStr(# the carrier of C2, the Arrows of C2, the Comp of C2 #)
proofend;

registration
let C be AltCatStr ;
cluster strict for SubCatStr of C;
existence
 ex b1 being SubCatStr of C st b1 is strict
proofend;
end;

definition
let C be non empty AltCatStr ;
let o be object of C;
func ObCat o ->  strict SubCatStr of C means :Def12: :: ALTCAT_2:def 12
( the carrier of it = {o} &amp; the Arrows of it = (o,o) :-> <^o,o^> &amp; the Comp of it = [o,o,o] .--> ( the Comp of C . (o,o,o)) );
existence
 ex b1 being strict SubCatStr of C st
( the carrier of b1 = {o} &amp; the Arrows of b1 = (o,o) :-> <^o,o^> &amp; the Comp of b1 = [o,o,o] .--> ( the Comp of C . (o,o,o)) )
proofend;
uniqueness
 for b1, b2 being strict SubCatStr of C st the carrier of b1 = {o} &amp; the Arrows of b1 = (o,o) :-> <^o,o^> &amp; the Comp of b1 = [o,o,o] .--> ( the Comp of C . (o,o,o)) &amp; the carrier of b2 = {o} &amp; the Arrows of b2 = (o,o) :-> <^o,o^> &amp; the Comp of b2 = [o,o,o] .--> ( the Comp of C . (o,o,o)) holds
b1 = b2 ;
end;

:: deftheorem Def12 defines ObCat ALTCAT_2:def_12_:_
 for C being non empty AltCatStr
for o being object of C
for b3 being strict SubCatStr of C holds
( b3 = ObCat o iff ( the carrier of b3 = {o} &amp; the Arrows of b3 = (o,o) :-> <^o,o^> &amp; the Comp of b3 = [o,o,o] .--> ( the Comp of C . (o,o,o)) ) );

theorem Th23: :: ALTCAT_2:23
for C being non empty AltCatStr
for o being object of C
for o9 being object of (ObCat o) holds o9 = o
proofend;

registration
let C be non empty AltCatStr ;
let o be object of C;
cluster ObCat o ->  non empty transitive strict ;
coherence
 ( ObCat o is transitive &amp; not ObCat o is empty )
proofend;
end;

registration
let C be non empty AltCatStr ;
cluster non empty transitive strict for SubCatStr of C;
existence
 ex b1 being SubCatStr of C st
( b1 is transitive &amp; not b1 is empty &amp; b1 is strict )
proofend;
end;

theorem Th24: :: ALTCAT_2:24
for C being non empty transitive AltCatStr
for D1, D2 being non empty transitive SubCatStr of C st the carrier of D1 c= the carrier of D2 &amp; the Arrows of D1 cc= the Arrows of D2 holds
D1 is SubCatStr of D2
proofend;

definition
let C be AltCatStr ;
let D be SubCatStr of C;
attrD is full  means :Def13: :: ALTCAT_2:def 13
 the Arrows of D = the Arrows of C || the carrier of D;
end;

:: deftheorem Def13 defines full ALTCAT_2:def_13_:_
 for C being AltCatStr
for D being SubCatStr of C holds
( D is full iff the Arrows of D = the Arrows of C || the carrier of D );

definition
let C be non empty with_units AltCatStr ;
let D be SubCatStr of C;
attrD is id-inheriting  means :Def14: :: ALTCAT_2:def 14
 for o being object of D
for o9 being object of C st o = o9 holds
idm o9 in <^o,o^> if  not D is empty
otherwise verum;
consistency
 verum ;
end;

:: deftheorem Def14 defines id-inheriting ALTCAT_2:def_14_:_
 for C being non empty with_units AltCatStr
for D being SubCatStr of C holds
( ( not D is empty implies ( D is id-inheriting iff for o being object of D
for o9 being object of C st o = o9 holds
idm o9 in <^o,o^> ) ) &amp; ( D is empty implies ( D is id-inheriting iff verum ) ) );

registration
let C be AltCatStr ;
cluster strict full for SubCatStr of C;
existence
 ex b1 being SubCatStr of C st
( b1 is full &amp; b1 is strict )
proofend;
end;

registration
let C be non empty AltCatStr ;
cluster non empty strict full for SubCatStr of C;
existence
 ex b1 being SubCatStr of C st
( b1 is full &amp; not b1 is empty &amp; b1 is strict )
proofend;
end;

registration
let C be category;
let o be object of C;
cluster ObCat o ->  strict full id-inheriting ;
coherence
 ( ObCat o is full &amp; ObCat o is id-inheriting )
proofend;
end;

registration
let C be category;
cluster non empty strict full id-inheriting for SubCatStr of C;
existence
 ex b1 being SubCatStr of C st
( b1 is full &amp; b1 is id-inheriting &amp; not b1 is empty &amp; b1 is strict )
proofend;
end;

theorem Th25: :: ALTCAT_2:25
for C being non empty transitive AltCatStr
for D being SubCatStr of C st the carrier of D = the carrier of C &amp; the Arrows of D = the Arrows of C holds
AltCatStr(# the carrier of D, the Arrows of D, the Comp of D #) = AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #)
proofend;

theorem Th26: :: ALTCAT_2:26
for C being non empty transitive AltCatStr
for D1, D2 being non empty transitive SubCatStr of C st the carrier of D1 = the carrier of D2 &amp; the Arrows of D1 = the Arrows of D2 holds
AltCatStr(# the carrier of D1, the Arrows of D1, the Comp of D1 #) = AltCatStr(# the carrier of D2, the Arrows of D2, the Comp of D2 #)
proofend;

theorem :: ALTCAT_2:27
for C being non empty transitive AltCatStr
for D being full SubCatStr of C st the carrier of D = the carrier of C holds
AltCatStr(# the carrier of D, the Arrows of D, the Comp of D #) = AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #)
proofend;

theorem Th28: :: ALTCAT_2:28
for C being non empty AltCatStr
for D being non empty full SubCatStr of C
for o1, o2 being object of C
for p1, p2 being object of D st o1 = p1 &amp; o2 = p2 holds
<^o1,o2^> = <^p1,p2^>
proofend;

theorem Th29: :: ALTCAT_2:29
for C being non empty AltCatStr
for D being non empty SubCatStr of C
for o being object of D holds o is object of C
proofend;

registration
let C be non empty transitive AltCatStr ;
cluster non empty full  ->  transitive for SubCatStr of C;
coherence
 for b1 being SubCatStr of C st b1 is full &amp; not b1 is empty holds
b1 is transitive
proofend;
end;

theorem :: ALTCAT_2:30
for C being non empty transitive AltCatStr
for D1, D2 being non empty full SubCatStr of C st the carrier of D1 = the carrier of D2 holds
AltCatStr(# the carrier of D1, the Arrows of D1, the Comp of D1 #) = AltCatStr(# the carrier of D2, the Arrows of D2, the Comp of D2 #)
proofend;

theorem Th31: :: ALTCAT_2:31
for C being non empty AltCatStr
for D being non empty SubCatStr of C
for o1, o2 being object of C
for p1, p2 being object of D st o1 = p1 &amp; o2 = p2 holds
<^p1,p2^> c= <^o1,o2^>
proofend;

theorem Th32: :: ALTCAT_2:32
for C being non empty transitive AltCatStr
for D being non empty transitive SubCatStr of C
for p1, p2, p3 being object of D st <^p1,p2^> <> {} &amp; <^p2,p3^> <> {} holds
for o1, o2, o3 being object of C st o1 = p1 &amp; o2 = p2 &amp; o3 = p3 holds
for f being Morphism of o1,o2
for g being Morphism of o2,o3
for ff being Morphism of p1,p2
for gg being Morphism of p2,p3 st f = ff &amp; g = gg holds
g * f = gg * ff
proofend;

registration
let C be non empty transitive associative AltCatStr ;
cluster non empty transitive  ->  non empty associative for SubCatStr of C;
coherence
 for b1 being non empty SubCatStr of C st b1 is transitive holds
b1 is associative
proofend;
end;

theorem Th33: :: ALTCAT_2:33
for C being non empty AltCatStr
for D being non empty SubCatStr of C
for o1, o2 being object of C
for p1, p2 being object of D st o1 = p1 &amp; o2 = p2 &amp; <^p1,p2^> <> {} holds
for n being Morphism of p1,p2 holds n is Morphism of o1,o2
proofend;

registration
let C be non empty transitive with_units AltCatStr ;
cluster non empty transitive id-inheriting  ->  non empty with_units for SubCatStr of C;
coherence
 for b1 being non empty SubCatStr of C st b1 is id-inheriting &amp; b1 is transitive holds
b1 is with_units
proofend;
end;

registration
let C be category;
cluster non empty transitive id-inheriting for SubCatStr of C;
existence
 ex b1 being non empty SubCatStr of C st
( b1 is id-inheriting &amp; b1 is transitive )
proofend;
end;

definition
let C be category;
mode subcategory of C is transitive id-inheriting SubCatStr of C;
end;

theorem :: ALTCAT_2:34
for C being category
for D being non empty subcategory of C
for o being object of D
for o9 being object of C st o = o9 holds
idm o = idm o9
proofend;