let C be Category; for b being Object of C holds
( b is terminal iff for a being Object of C ex f being Morphism of a,b st Hom (a,b) = {f} )
let b be Object of C; ( b is terminal iff for a being Object of C ex f being Morphism of a,b st Hom (a,b) = {f} )
thus
( b is terminal implies for a being Object of C ex f being Morphism of a,b st Hom (a,b) = {f} )
( ( for a being Object of C ex f being Morphism of a,b st Hom (a,b) = {f} ) implies b is terminal )proof
assume A1:
b is
terminal
;
for a being Object of C ex f being Morphism of a,b st Hom (a,b) = {f}
let a be
Object of
C;
ex f being Morphism of a,b st Hom (a,b) = {f}
consider f being
Morphism of
a,
b such that A2:
for
g being
Morphism of
a,
b holds
f = g
by A1;
take
f
;
Hom (a,b) = {f}
thus
Hom (
a,
b)
= {f}
by A2, Th7, A1;
verum
end;
assume A3:
for a being Object of C ex f being Morphism of a,b st Hom (a,b) = {f}
; b is terminal
let a be Object of C; CAT_1:def 18 ( Hom (a,b) <> {} & ex f being Morphism of a,b st
for g being Morphism of a,b holds f = g )
consider f being Morphism of a,b such that
A4:
Hom (a,b) = {f}
by A3;
thus
Hom (a,b) <> {}
by A4; ex f being Morphism of a,b st
for g being Morphism of a,b holds f = g
take
f
; for g being Morphism of a,b holds f = g
thus
for g being Morphism of a,b holds f = g
by A4, Th6; verum