begin
begin
begin
begin
definition
let C be non
empty non
void CatStr ;
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)
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
end;
definition
let C be
Category;
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)):]
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
end;
begin
begin
begin
Lm1:
for E1, E2 being strict AltCatStr st the carrier of E1 is empty & the carrier of E2 is empty holds
E1 = E2
begin
definition
let C be non
empty AltCatStr ;
let o be
object of
C;
existence
ex b1 being strict SubCatStr of C st
( the carrier of b1 = {o} & the Arrows of b1 = (o,o) :-> <^o,o^> & the Comp of b1 = [o,o,o] .--> ( the Comp of C . (o,o,o)) )
uniqueness
for b1, b2 being strict SubCatStr of C st the carrier of b1 = {o} & the Arrows of b1 = (o,o) :-> <^o,o^> & the Comp of b1 = [o,o,o] .--> ( the Comp of C . (o,o,o)) & the carrier of b2 = {o} & the Arrows of b2 = (o,o) :-> <^o,o^> & the Comp of b2 = [o,o,o] .--> ( the Comp of C . (o,o,o)) holds
b1 = b2
;
end;
theorem Th32:
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