let C be Category; for a being Object of C holds
( a is initial iff for b being Object of C ex f being Morphism of a,b st Hom (a,b) = {f} )
let a be Object of C; ( a is initial iff for b being Object of C ex f being Morphism of a,b st Hom (a,b) = {f} )
thus
( a is initial implies for b being Object of C ex f being Morphism of a,b st Hom (a,b) = {f} )
( ( for b being Object of C ex f being Morphism of a,b st Hom (a,b) = {f} ) implies a is initial )proof
assume A1:
a is
initial
;
for b being Object of C ex f being Morphism of a,b st Hom (a,b) = {f}
let b 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 b being Object of C ex f being Morphism of a,b st Hom (a,b) = {f}
; a is initial
let b be Object of C; CAT_1:def 19 ( 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