let C, D be Category; :: thesis: for c, c' being Object of C
for f being Morphism of c,c'
for d, d' being Object of D
for g being Morphism of d,d' st Hom c,c' <> {} & Hom d,d' <> {} holds
[f,g] is Morphism of [c,d],[c',d']
let c, c' be Object of C; :: thesis: for f being Morphism of c,c'
for d, d' being Object of D
for g being Morphism of d,d' st Hom c,c' <> {} & Hom d,d' <> {} holds
[f,g] is Morphism of [c,d],[c',d']
let f be Morphism of c,c'; :: thesis: for d, d' being Object of D
for g being Morphism of d,d' st Hom c,c' <> {} & Hom d,d' <> {} holds
[f,g] is Morphism of [c,d],[c',d']
let d, d' be Object of D; :: thesis: for g being Morphism of d,d' st Hom c,c' <> {} & Hom d,d' <> {} holds
[f,g] is Morphism of [c,d],[c',d']
let g be Morphism of d,d'; :: thesis: ( Hom c,c' <> {} & Hom d,d' <> {} implies [f,g] is Morphism of [c,d],[c',d'] )
assume ( Hom c,c' <> {} & Hom d,d' <> {} ) ; :: thesis: [f,g] is Morphism of [c,d],[c',d']
then ( dom f = c & cod f = c' & dom g = d & cod g = d' ) by CAT_1:23;
then ( dom [f,g] = [c,d] & cod [f,g] = [c',d'] ) by Th38;
hence [f,g] is Morphism of [c,d],[c',d'] by CAT_1:22; :: thesis: verum