let C, D be Category; :: thesis: for c, c9 being Object of C
for f being Morphism of c,c9
for d, d9 being Object of D
for g being Morphism of d,d9 st Hom (c,c9) <> {} & Hom (d,d9) <> {} holds
[f,g] is Morphism of [c,d],[c9,d9]
let c, c9 be Object of C; :: thesis: for f being Morphism of c,c9
for d, d9 being Object of D
for g being Morphism of d,d9 st Hom (c,c9) <> {} & Hom (d,d9) <> {} holds
[f,g] is Morphism of [c,d],[c9,d9]
let f be Morphism of c,c9; :: thesis: for d, d9 being Object of D
for g being Morphism of d,d9 st Hom (c,c9) <> {} & Hom (d,d9) <> {} holds
[f,g] is Morphism of [c,d],[c9,d9]
let d, d9 be Object of D; :: thesis: for g being Morphism of d,d9 st Hom (c,c9) <> {} & Hom (d,d9) <> {} holds
[f,g] is Morphism of [c,d],[c9,d9]
let g be Morphism of d,d9; :: thesis: ( Hom (c,c9) <> {} & Hom (d,d9) <> {} implies [f,g] is Morphism of [c,d],[c9,d9] )
assume A1: ( Hom (c,c9) <> {} & Hom (d,d9) <> {} ) ; :: thesis: [f,g] is Morphism of [c,d],[c9,d9]
then ( cod f = c9 & cod g = d9 ) by CAT_1:5;
then A2: cod [f,g] = [c9,d9] by Th22;
( dom f = c & dom g = d ) by A1, CAT_1:5;
then dom [f,g] = [c,d] by Th22;
hence [f,g] is Morphism of [c,d],[c9,d9] by A2, CAT_1:4; :: thesis: verum