let C, D be Category; :: thesis: for c, c9 being Object of C
for d, d9 being Object of D holds Hom ([c,d],[c9,d9]) = [:(Hom (c,c9)),(Hom (d,d9)):]
let c, c9 be Object of C; :: thesis: for d, d9 being Object of D holds Hom ([c,d],[c9,d9]) = [:(Hom (c,c9)),(Hom (d,d9)):]
let d, d9 be Object of D; :: thesis: Hom ([c,d],[c9,d9]) = [:(Hom (c,c9)),(Hom (d,d9)):]

now :: thesis: for x being object holds
( ( x in Hom ([c,d],[c9,d9]) implies x in [:(Hom (c,c9)),(Hom (d,d9)):] ) & ( x in [:(Hom (c,c9)),(Hom (d,d9)):] implies x in Hom ([c,d],[c9,d9]) ) )

let x be object ; :: thesis: ( ( x in Hom ([c,d],[c9,d9]) implies x in [:(Hom (c,c9)),(Hom (d,d9)):] ) & ( x in [:(Hom (c,c9)),(Hom (d,d9)):] implies x in Hom ([c,d],[c9,d9]) ) )
thus ( x in Hom ([c,d],[c9,d9]) implies x in [:(Hom (c,c9)),(Hom (d,d9)):] ) :: thesis: ( x in [:(Hom (c,c9)),(Hom (d,d9)):] implies x in Hom ([c,d],[c9,d9]) )

proof

assume A1: x in Hom ([c,d],[c9,d9]) ; :: thesis: x in [:(Hom (c,c9)),(Hom (d,d9)):]
then reconsider fg = x as Morphism of [c,d],[c9,d9] by CAT_1:def 5;
A2: dom fg = [c,d] by A1, CAT_1:1;
A3: cod fg = [c9,d9] by A1, CAT_1:1;
consider x1, x2 being object such that
A4: x1 in the carrier' of C and
A5: x2 in the carrier' of D and
A6: fg = [x1,x2] by ZFMISC_1:def 2;
reconsider g = x2 as Morphism of D by A5;
reconsider f = x1 as Morphism of C by A4;
A7: cod fg = [(cod f),(cod g)] by A6, Th22;
then A8: cod f = c9 by A3, XTUPLE_0:1;
A9: cod g = d9 by A3, A7, XTUPLE_0:1;
A10: dom fg = [(dom f),(dom g)] by A6, Th22;
then dom g = d by A2, XTUPLE_0:1;
then A11: g in Hom (d,d9) by A9;
dom f = c by A2, A10, XTUPLE_0:1;
then f in Hom (c,c9) by A8;
hence x in [:(Hom (c,c9)),(Hom (d,d9)):] by A6, A11, ZFMISC_1:87; :: thesis: verum

end;

assume x in [:(Hom (c,c9)),(Hom (d,d9)):] ; :: thesis: x in Hom ([c,d],[c9,d9])
then consider x1, x2 being object such that
A12: x1 in Hom (c,c9) and
A13: x2 in Hom (d,d9) and
A14: x = [x1,x2] by ZFMISC_1:def 2;
reconsider g = x2 as Morphism of d,d9 by A13, CAT_1:def 5;
reconsider f = x1 as Morphism of c,c9 by A12, CAT_1:def 5;
( cod f = c9 & cod g = d9 ) by A12, A13, CAT_1:1;
then A15: cod [f,g] = [c9,d9] by Th22;
( dom f = c & dom g = d ) by A12, A13, CAT_1:1;
then dom [f,g] = [c,d] by Th22;
hence x in Hom ([c,d],[c9,d9]) by A14, A15; :: thesis: verum

end;

hence Hom ([c,d],[c9,d9]) = [:(Hom (c,c9)),(Hom (d,d9)):] by TARSKI:2; :: thesis: verum