let C be non empty non void CatStr ; 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; 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; 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; ( Hom (a,b) <> {} & Hom (c,d) <> {} & f = h implies ( a = c & b = d ) )
assume that
A1:
Hom (a,b) <> {}
and
A2:
Hom (c,d) <> {}
; ( 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; verum