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:4;
then F . f in Hom (c,d) by TARSKI:def 1;
then F . f is Morphism of c,d by Def3;
hence ex h being Morphism of c,d st Hom (c,d) = {h} by A2; :: thesis: verum