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, Th23;
hence ( not f = h or ( a = c & b = d ) ) by A2, Th23; :: thesis: verum