begin
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 Def5e;
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;