let C be non empty non void CatStr ; :: 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 set holds
( x in Hom a,b iff x = f )

proof

let x be set ; :: 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 consider g being Morphism of C such that
A3: x = g and
A4: ( dom g = a & cod g = b ) ;
g is Morphism of a,b by A4, Th22;
hence x = f by A2, A3; :: thesis: verum

end;

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

end;

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