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

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