let C be CategoryStr ; :: thesis: for a, b being Object of C
for f being Morphism of a,b st Hom (a,b) = {f} holds
for g being Morphism of a,b holds f = g
let a, b be Object of C; :: thesis: for f being Morphism of a,b st Hom (a,b) = {f} holds
for g being Morphism of a,b holds f = g
let f be Morphism of a,b; :: thesis: ( Hom (a,b) = {f} implies for g being Morphism of a,b holds f = g )
assume A1: Hom (a,b) = {f} ; :: thesis: for g being Morphism of a,b holds f = g
let g be Morphism of a,b; :: thesis: f = g
g in {f} by A1, CAT_7:def 3;
hence f = g by TARSKI:def 1; :: thesis: verum