:: by Andrzej Trybulec

::

:: Received January 22, 1996

:: Copyright (c) 1996-2012 Association of Mizar Users

begin

registration
end;

registration
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

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

proof end;

registration
end;

registration

let I be set ;

let A be ManySortedSet of [:I,I:];

coherence

for b_{1} being [:I,I:] -defined Function st b_{1} = ~ A holds

b_{1} is total
;

end;
let A be ManySortedSet of [:I,I:];

coherence

for b

b

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

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

proof end;

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

end;
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

proof 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)

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)

proof end;

registration
end;

registration
end;

begin

definition

let f, g be Function;

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;
pred f 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 ( dom f c= dom g & ( for i being set st i in dom f holds

f . i c= g . i ) );

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 ) ) ;

:: 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 ) ) );

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;

( A cc= B iff ( I c= J & ( for i being set st i in I holds

A . i c= B . i ) ) )

end;
let A be ManySortedSet of I;

let B be ManySortedSet of J;

:: original: cc=

redefine pred A 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 redefine pred A 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 ) );

( A cc= B iff ( I c= J & ( for i being set st i in I holds

A . i c= B . i ) ) )

proof 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 ) ) );

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

for A being ManySortedSet of I

for B being ManySortedSet of J st A cc= B & B cc= A holds

A = B

proof end;

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

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

proof end;

begin

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

for i, j, k being Object of C holds [:(Hom (j,k)),(Hom (i,j)):] c= dom the Comp of C

proof end;

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)

for i, j, k being Object of C holds the Comp of C .: [:(Hom (j,k)),(Hom (i,j)):] c= Hom (i,k)

proof end;

definition

let C be non empty non void CatStr ;

ex b_{1} being ManySortedSet of [: the carrier of C, the carrier of C:] st

for i, j being Object of C holds b_{1} . (i,j) = Hom (i,j)

for b_{1}, b_{2} being ManySortedSet of [: the carrier of C, the carrier of C:] st ( for i, j being Object of C holds b_{1} . (i,j) = Hom (i,j) ) & ( for i, j being Object of C holds b_{2} . (i,j) = Hom (i,j) ) holds

b_{1} = b_{2}

end;
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 for i, j being Object of C holds it . (i,j) = Hom (i,j);

ex b

for i, j being Object of C holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def3 defines the_hom_sets_of ALTCAT_2:def 3 :

for C being non empty non void CatStr

for b_{2} being ManySortedSet of [: the carrier of C, the carrier of C:] holds

( b_{2} = the_hom_sets_of C iff for i, j being Object of C holds b_{2} . (i,j) = Hom (i,j) );

for C being non empty non void CatStr

for b

( b

definition

let C be Category;

ex b_{1} being BinComp of (the_hom_sets_of C) st

for i, j, k being Object of C holds b_{1} . (i,j,k) = the Comp of C | [:((the_hom_sets_of C) . (j,k)),((the_hom_sets_of C) . (i,j)):]

for b_{1}, b_{2} being BinComp of (the_hom_sets_of C) st ( for i, j, k being Object of C holds b_{1} . (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 b_{2} . (i,j,k) = the Comp of C | [:((the_hom_sets_of C) . (j,k)),((the_hom_sets_of C) . (i,j)):] ) holds

b_{1} = b_{2}

end;
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 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)):];

ex b

for i, j, k being Object of C holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def4 defines the_comps_of ALTCAT_2:def 4 :

for C being Category

for b_{2} being BinComp of (the_hom_sets_of C) holds

( b_{2} = the_comps_of C iff for i, j, k being Object of C holds b_{2} . (i,j,k) = the Comp of C | [:((the_hom_sets_of C) . (j,k)),((the_hom_sets_of C) . (i,j)):] );

for C being Category

for b

( b

theorem Th13: :: ALTCAT_2:13

for C being Category

for i, j, k being Object of C st Hom (i,j) <> {} & 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

for i, j, k being Object of C st Hom (i,j) <> {} & 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

proof end;

theorem Th15: :: ALTCAT_2:15

for C being Category holds

( the_comps_of C is with_left_units & the_comps_of C is with_right_units )

( the_comps_of C is with_left_units & the_comps_of C is with_right_units )

proof end;

begin

definition

let C be Category;

coherence

AltCatStr(# the carrier of C,(the_hom_sets_of C),(the_comps_of C) #) is non empty strict AltCatStr ;

;

end;
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 AltCatStr(# the carrier of C,(the_hom_sets_of C),(the_comps_of C) #);

coherence

AltCatStr(# the carrier of C,(the_hom_sets_of C),(the_comps_of C) #) is non empty strict AltCatStr ;

;

:: 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) #);

for C being Category holds Alter C = AltCatStr(# the carrier of C,(the_hom_sets_of C),(the_comps_of C) #);

registration

let C be Category;

coherence

( Alter C is transitive & Alter C is associative & Alter C is with_units ) by Th16, Th17, Th18;

end;
coherence

( Alter C is transitive & Alter C is associative & Alter C is with_units ) by Th16, Th17, Th18;

begin

registration
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) <> {} );

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 ;

compatibility

( C is reflexive iff for o being object of C holds <^o,o^> <> {} )

end;
compatibility

( C is reflexive iff for o being object of C holds <^o,o^> <> {} )

proof 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^> <> {} );

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 ;

( 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^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} holds

(h * g) * f = h * (g * f) )

end;
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^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} holds

(h * g) * f = h * (g * f);

compatibility 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^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} holds

(h * g) * f = h * (g * f);

( 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^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} holds

(h * g) * f = h * (g * f) )

proof 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^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} holds

(h * g) * f = h * (g * f) );

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^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} holds

(h * g) * f = h * (g * f) );

definition

let C be non empty AltCatStr ;

( C is with_units iff for o being object of C holds

( <^o,o^> <> {} & 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 ) & ( <^o,o9^> <> {} implies m99 * i = m99 ) ) ) )

end;
redefine attr C is with_units means :: ALTCAT_2:def 9

for o being object of C holds

( <^o,o^> <> {} & 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 ) & ( <^o,o9^> <> {} implies m99 * i = m99 ) ) );

compatibility for o being object of C holds

( <^o,o^> <> {} & 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 ) & ( <^o,o9^> <> {} implies m99 * i = m99 ) ) );

( C is with_units iff for o being object of C holds

( <^o,o^> <> {} & 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 ) & ( <^o,o9^> <> {} implies m99 * i = m99 ) ) ) )

proof 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^> <> {} & 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 ) & ( <^o,o9^> <> {} implies m99 * i = m99 ) ) ) );

for C being non empty AltCatStr holds

( C is with_units iff for o being object of C holds

( <^o,o^> <> {} & 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 ) & ( <^o,o9^> <> {} implies m99 * i = m99 ) ) ) );

registration

coherence

for b_{1} being non empty AltCatStr st b_{1} is with_units holds

b_{1} is reflexive

end;
for b

b

proof end;

registration
end;

registration
end;

begin

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

E1 = E2

proof end;

definition

ex b_{1} being strict AltCatStr st the carrier of b_{1} is empty

for b_{1}, b_{2} being strict AltCatStr st the carrier of b_{1} is empty & the carrier of b_{2} is empty holds

b_{1} = b_{2}
by Lm1;

end;

func the_empty_category -> strict AltCatStr means :Def10: :: ALTCAT_2:def 10

the carrier of it is empty ;

existence the carrier of it is empty ;

ex b

proof end;

uniqueness for b

b

:: deftheorem Def10 defines the_empty_category ALTCAT_2:def 10 :

for b_{1} being strict AltCatStr holds

( b_{1} = the_empty_category iff the carrier of b_{1} is empty );

for b

( b

registration
end;

registration
end;

begin

:: Semadeni Wiweger 1.6.1 str. 24

definition

let C be AltCatStr ;

ex b_{1} being AltCatStr st

( the carrier of b_{1} c= the carrier of C & the Arrows of b_{1} cc= the Arrows of C & the Comp of b_{1} cc= the Comp of C )
;

end;
mode SubCatStr of C -> AltCatStr means :Def11: :: ALTCAT_2:def 11

( the carrier of it c= the carrier of C & the Arrows of it cc= the Arrows of C & the Comp of it cc= the Comp of C );

existence ( the carrier of it c= the carrier of C & the Arrows of it cc= the Arrows of C & the Comp of it cc= the Comp of C );

ex b

( the carrier of b

:: deftheorem Def11 defines SubCatStr ALTCAT_2:def 11 :

for C, b_{2} being AltCatStr holds

( b_{2} is SubCatStr of C iff ( the carrier of b_{2} c= the carrier of C & the Arrows of b_{2} cc= the Arrows of C & the Comp of b_{2} cc= the Comp of C ) );

for C, b

( b

theorem :: ALTCAT_2:21

for C1, C2, C3 being AltCatStr st C1 is SubCatStr of C2 & C2 is SubCatStr of C3 holds

C1 is SubCatStr of C3

C1 is SubCatStr of C3

proof end;

theorem Th22: :: ALTCAT_2:22

for C1, C2 being AltCatStr st C1 is SubCatStr of C2 & 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 #)

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 #)

proof end;

registration
end;

definition

let C be non empty AltCatStr ;

let o be object of C;

ex b_{1} being strict SubCatStr of C st

( the carrier of b_{1} = {o} & the Arrows of b_{1} = (o,o) :-> <^o,o^> & the Comp of b_{1} = [o,o,o] .--> ( the Comp of C . (o,o,o)) )

for b_{1}, b_{2} being strict SubCatStr of C st the carrier of b_{1} = {o} & the Arrows of b_{1} = (o,o) :-> <^o,o^> & the Comp of b_{1} = [o,o,o] .--> ( the Comp of C . (o,o,o)) & the carrier of b_{2} = {o} & the Arrows of b_{2} = (o,o) :-> <^o,o^> & the Comp of b_{2} = [o,o,o] .--> ( the Comp of C . (o,o,o)) holds

b_{1} = b_{2}
;

end;
let o be object of C;

func ObCat o -> strict SubCatStr of C means :Def12: :: ALTCAT_2:def 12

( the carrier of it = {o} & the Arrows of it = (o,o) :-> <^o,o^> & the Comp of it = [o,o,o] .--> ( the Comp of C . (o,o,o)) );

existence ( the carrier of it = {o} & the Arrows of it = (o,o) :-> <^o,o^> & the Comp of it = [o,o,o] .--> ( the Comp of C . (o,o,o)) );

ex b

( the carrier of b

proof end;

uniqueness for b

b

:: deftheorem Def12 defines ObCat ALTCAT_2:def 12 :

for C being non empty AltCatStr

for o being object of C

for b_{3} being strict SubCatStr of C holds

( b_{3} = ObCat o iff ( the carrier of b_{3} = {o} & the Arrows of b_{3} = (o,o) :-> <^o,o^> & the Comp of b_{3} = [o,o,o] .--> ( the Comp of C . (o,o,o)) ) );

for C being non empty AltCatStr

for o being object of C

for b

( b

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

for o being object of C

for o9 being object of (ObCat o) holds o9 = o

proof end;

registration

let C be non empty AltCatStr ;

let o be object of C;

coherence

( ObCat o is transitive & not ObCat o is empty )

end;
let o be object of C;

coherence

( ObCat o is transitive & not ObCat o is empty )

proof end;

registration

let C be non empty AltCatStr ;

existence

ex b_{1} being SubCatStr of C st

( b_{1} is transitive & not b_{1} is empty & b_{1} is strict )

end;
existence

ex b

( b

proof 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 & the Arrows of D1 cc= the Arrows of D2 holds

D1 is SubCatStr of D2

for D1, D2 being non empty transitive SubCatStr of C st the carrier of D1 c= the carrier of D2 & the Arrows of D1 cc= the Arrows of D2 holds

D1 is SubCatStr of D2

proof 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 );

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;

verum ;

end;
let D be SubCatStr of C;

attr D 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 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;

verum ;

:: 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^> ) ) & ( D is empty implies ( D is id-inheriting iff verum ) ) );

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^> ) ) & ( D is empty implies ( D is id-inheriting iff verum ) ) );

registration

let C be AltCatStr ;

existence

ex b_{1} being SubCatStr of C st

( b_{1} is full & b_{1} is strict )

end;
existence

ex b

( b

proof end;

registration

let C be non empty AltCatStr ;

existence

ex b_{1} being SubCatStr of C st

( b_{1} is full & not b_{1} is empty & b_{1} is strict )

end;
existence

ex b

( b

proof end;

registration

let C be category;

let o be object of C;

coherence

( ObCat o is full & ObCat o is id-inheriting )

end;
let o be object of C;

coherence

( ObCat o is full & ObCat o is id-inheriting )

proof end;

registration

let C be category;

existence

ex b_{1} being SubCatStr of C st

( b_{1} is full & b_{1} is id-inheriting & not b_{1} is empty & b_{1} is strict )

end;
existence

ex b

( b

proof 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 & 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 #)

for D being SubCatStr of C st the carrier of D = the carrier of C & 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 #)

proof end;

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 & 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 #)

for D1, D2 being non empty transitive SubCatStr of C st the carrier of D1 = the carrier of D2 & 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 #)

proof end;

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 #)

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 #)

proof end;

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 & o2 = p2 holds

<^o1,o2^> = <^p1,p2^>

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 & o2 = p2 holds

<^o1,o2^> = <^p1,p2^>

proof end;

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

for D being non empty SubCatStr of C

for o being object of D holds o is object of C

proof end;

registration

let C be non empty transitive AltCatStr ;

coherence

for b_{1} being SubCatStr of C st b_{1} is full & not b_{1} is empty holds

b_{1} is transitive

end;
coherence

for b

b

proof 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 #)

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 #)

proof end;

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 & o2 = p2 holds

<^p1,p2^> c= <^o1,o2^>

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 & o2 = p2 holds

<^p1,p2^> c= <^o1,o2^>

proof end;

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^> <> {} & <^p2,p3^> <> {} holds

for o1, o2, o3 being object of C st o1 = p1 & o2 = p2 & 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 & g = gg holds

g * f = gg * ff

for D being non empty transitive SubCatStr of C

for p1, p2, p3 being object of D st <^p1,p2^> <> {} & <^p2,p3^> <> {} holds

for o1, o2, o3 being object of C st o1 = p1 & o2 = p2 & 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 & g = gg holds

g * f = gg * ff

proof end;

registration

let C be non empty transitive associative AltCatStr ;

coherence

for b_{1} being non empty SubCatStr of C st b_{1} is transitive holds

b_{1} is associative

end;
coherence

for b

b

proof 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 & o2 = p2 & <^p1,p2^> <> {} holds

for n being Morphism of p1,p2 holds n is Morphism of o1,o2

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 & o2 = p2 & <^p1,p2^> <> {} holds

for n being Morphism of p1,p2 holds n is Morphism of o1,o2

proof end;

registration

let C be non empty transitive with_units AltCatStr ;

coherence

for b_{1} being non empty SubCatStr of C st b_{1} is id-inheriting & b_{1} is transitive holds

b_{1} is with_units

end;
coherence

for b

b

proof end;

registration

let C be category;

existence

ex b_{1} being non empty SubCatStr of C st

( b_{1} is id-inheriting & b_{1} is transitive )

end;
existence

ex b

( b

proof 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

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

proof end;