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

now

let x be set ; :: thesis: ( ( x in Hom [c,d],[c',d'] implies x in [:(Hom c,c'),(Hom d,d'):] ) & ( x in [:(Hom c,c'),(Hom d,d'):] implies x in Hom [c,d],[c',d'] ) )
thus ( x in Hom [c,d],[c',d'] implies x in [:(Hom c,c'),(Hom d,d'):] ) :: thesis: ( x in [:(Hom c,c'),(Hom d,d'):] implies x in Hom [c,d],[c',d'] )

proof

assume A1: x in Hom [c,d],[c',d'] ; :: thesis: x in [:(Hom c,c'),(Hom d,d'):]
then reconsider fg = x as Morphism of [c,d],[c',d'] by CAT_1:def 7;
A2: dom fg = [c,d] by A1, CAT_1:18;
A3: cod fg = [c',d'] by A1, CAT_1:18;
consider x1, x2 being set 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 by A5;
reconsider f = x1 as Morphism of by A4;
A7: cod fg = [(cod f),(cod g)] by A6, Th38;
then A8: cod f = c' by A3, ZFMISC_1:33;
A9: cod g = d' by A3, A7, ZFMISC_1:33;
A10: dom fg = [(dom f),(dom g)] by A6, Th38;
then dom g = d by A2, ZFMISC_1:33;
then A11: g in Hom d,d' by A9;
dom f = c by A2, A10, ZFMISC_1:33;
then f in Hom c,c' by A8;
hence x in [:(Hom c,c'),(Hom d,d'):] by A6, A11, ZFMISC_1:106; :: thesis: verum

end;

assume x in [:(Hom c,c'),(Hom d,d'):] ; :: thesis: x in Hom [c,d],[c',d']
then consider x1, x2 being set such that
A12: x1 in Hom c,c' and
A13: x2 in Hom d,d' and
A14: x = [x1,x2] by ZFMISC_1:def 2;
reconsider g = x2 as Morphism of d,d' by A13, CAT_1:def 7;
reconsider f = x1 as Morphism of c,c' by A12, CAT_1:def 7;
( cod f = c' & cod g = d' ) by A12, A13, CAT_1:18;
then A15: cod [f,g] = [c',d'] by Th38;
( dom f = c & dom g = d ) by A12, A13, CAT_1:18;
then dom [f,g] = [c,d] by Th38;
hence x in Hom [c,d],[c',d'] by A14, A15; :: thesis: verum

end;

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