let C, D be Category; 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; 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; 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; 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; ( Hom (c,c9) <> {} & Hom (d,d9) <> {} implies [f,g] is Morphism of [c,d],[c9,d9] )
assume A1:
( Hom (c,c9) <> {} & Hom (d,d9) <> {} )
; [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; verum