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
for h being Morphism of c,d st Hom a,b <> {} & Hom c,d <> {} & f = h holds
( a = c & b = d )
let a, b, c, d be Object of C; :: thesis: for f being Morphism of a,b
for h being Morphism of c,d st Hom a,b <> {} & Hom c,d <> {} & f = h holds
( a = c & b = d )
let f be Morphism of a,b; :: thesis: for h being Morphism of c,d st Hom a,b <> {} & Hom c,d <> {} & f = h holds
( a = c & b = d )
let h be Morphism of c,d; :: thesis: ( Hom a,b <> {} & Hom c,d <> {} & f = h implies ( a = c & b = d ) )
assume ( Hom a,b <> {} & Hom c,d <> {} ) ; :: thesis: ( not f = h or ( a = c & b = d ) )
then ( dom f = a & cod f = b & dom h = c & cod h = d ) by Th23;
hence ( not f = h or ( a = c & b = d ) ) ; :: thesis: verum