let C be non empty non void CatStr ; :: thesis: for a, b, c, d being Object of C
for f being Morphism of a,b st Hom a,b, Hom c,d are_equipotent & Hom a,b = {f} holds
ex h being Morphism of c,d st Hom c,d = {h}
let a, b, c, d be Object of C; :: thesis: for f being Morphism of a,b st Hom a,b, Hom c,d are_equipotent & Hom a,b = {f} holds
ex h being Morphism of c,d st Hom c,d = {h}
let f be Morphism of a,b; :: thesis: ( Hom a,b, Hom c,d are_equipotent & Hom a,b = {f} implies ex h being Morphism of c,d st Hom c,d = {h} )
assume Hom a,b, Hom c,d are_equipotent ; :: thesis: ( not Hom a,b = {f} or ex h being Morphism of c,d st Hom c,d = {h} )
then consider F being Function such that
F is one-to-one and
A1: ( dom F = Hom a,b & rng F = Hom c,d ) by WELLORD2:def 4;
assume Hom a,b = {f} ; :: thesis: ex h being Morphism of c,d st Hom c,d = {h}
then A2: Hom c,d = {(F . f)} by A1, FUNCT_1:14;
then F . f in Hom c,d by TARSKI:def 1;
then F . f is Morphism of c,d by Def7;
hence ex h being Morphism of c,d st Hom c,d = {h} by A2; :: thesis: verum