let C, D be Category; :: thesis: for c, c' being Object of
for f being Morphism of c,c'
for d, d' being Object of
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 ; :: thesis: for f being Morphism of c,c'
for d, d' being Object of
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
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 ; :: 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 A1: ( Hom c,c' <> {} & Hom d,d' <> {} ) ; :: thesis: [f,g] is Morphism of [c,d],[c',d']
then ( cod f = c' & cod g = d' ) by CAT_1:23;
then A2: cod [f,g] = [c',d'] by Th38;
( dom f = c & dom g = d ) by A1, CAT_1:23;
then dom [f,g] = [c,d] by Th38;
hence [f,g] is Morphism of [c,d],[c',d'] by A2, CAT_1:22; :: thesis: verum