environ
vocabularies HIDDEN, GRAPH_1, STRUCT_0, FUNCT_1, PARTFUN1, ZFMISC_1, SUBSET_1, XBOOLE_0, CARD_1, FUNCOP_1, RELAT_1, TARSKI, ALGSTR_0, WELLORD1, CAT_1, MONOID_0, RELAT_2, BINOP_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, ORDINAL1, NUMBERS, BINOP_1, FUNCOP_1, STRUCT_0, GRAPH_1;
definitions TARSKI, XBOOLE_0;
theorems TARSKI, FUNCT_1, FUNCT_2, PARTFUN1, FUNCOP_1, SUBSET_1, WELLORD2, ZFMISC_1, XBOOLE_0;
schemes FUNCT_2;
registrations XBOOLE_0, FUNCT_1, RELSET_1, FUNCT_2, STRUCT_0, RELAT_1, ZFMISC_1;
constructors HIDDEN, PARTFUN1, WELLORD2, BINOP_1, PBOOLE, GRAPH_1, RELSET_1, NUMBERS;
requirements HIDDEN, SUBSET, BOOLE;
equalities FUNCOP_1, BINOP_1, GRAPH_1;
expansions ;
theorem
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}
definition
let C be non
empty non
void reflexive with_identities CatStr ;
let a be
Object of
C;
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 Def8;
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
end;