let C be CategoryStr ; 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; 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; ( 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
; Hom (a,b) = {f}
for x being object holds
( x in Hom (a,b) iff x = f )
hence
Hom (a,b) = {f}
by TARSKI:def 1; verum