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 that
A1: Hom (a,b) <> {} and
A2: Hom (c,d) <> {} ; :: thesis: ( not f = h or ( a = c & b = d ) )
( dom f = a & cod f = b ) by A1, Th4;
hence ( not f = h or ( a = c & b = d ) ) by A2, Th4; :: thesis: verum