let C be CategoryStr ; :: thesis: for a, b being Object of C
for f being Morphism of a,b st Hom (a,b) <> {} & ( for g being Morphism of a,b holds f = g ) holds
Hom (a,b) = {f}
let a, b be Object of C; :: thesis: for f being Morphism of a,b st Hom (a,b) <> {} & ( for g being Morphism of a,b holds f = g ) holds
Hom (a,b) = {f}
let f be Morphism of a,b; :: thesis: ( Hom (a,b) <> {} & ( for g being Morphism of a,b holds f = g ) implies Hom (a,b) = {f} )
assume that
A1: Hom (a,b) <> {} and
A2: for g being Morphism of a,b holds f = g ; :: thesis: Hom (a,b) = {f}
for x being object holds
( x in Hom (a,b) iff x = f )

proof

let x be object ; :: thesis: ( x in Hom (a,b) iff x = f )
thus ( x in Hom (a,b) implies x = f ) :: thesis: ( x = f implies x in Hom (a,b) )

proof

assume x in Hom (a,b) ; :: thesis: x = f
then x in { f where f is morphism of C : ex f1, f2 being morphism of C st
( a = f1 & b = f2 & f |> f1 & f2 |> f ) } by CAT_7:def 1;
then consider g being morphism of C such that
A3: x = g and
A4: ex f1, f2 being morphism of C st
( a = f1 & b = f2 & g |> f1 & f2 |> g ) ;
g in { f where f is morphism of C : ex f1, f2 being morphism of C st
( a = f1 & b = f2 & f |> f1 & f2 |> f ) } by A4;
then g in Hom (a,b) by CAT_7:def 1;
then g is Morphism of a,b by CAT_7:def 3;
hence x = f by A2, A3; :: thesis: verum

end;

thus ( x = f implies x in Hom (a,b) ) by A1, CAT_7:def 3; :: thesis: verum

end;

hence Hom (a,b) = {f} by TARSKI:def 1; :: thesis: verum