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 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 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, Th3;
hence x = f by A2, A3; :: thesis: verum
end;
thus ( x = f implies x in Hom (a,b) ) by A1, Def3; :: thesis: verum
end;
hence Hom (a,b) = {f} by TARSKI:def 1; :: thesis: verum