let C, D be Category; :: thesis: for c, c' being Object of C
for d, d' being Object of D holds Hom [c,d],[c',d'] = [:(Hom c,c'),(Hom d,d'):]
let c, c' be Object of C; :: thesis: for d, d' being Object of D holds Hom [c,d],[c',d'] = [:(Hom c,c'),(Hom d,d'):]
let d, d' be Object of D; :: 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] & cod fg = [c',d'] ) by A1, CAT_1:18;
consider x1, x2 being set such that
A3: ( x1 in the carrier' of C & x2 in the carrier' of D ) and
A4: fg = [x1,x2] by ZFMISC_1:def 2;
reconsider f = x1 as Morphism of C by A3;
reconsider g = x2 as Morphism of D by A3;
( dom fg = [(dom f),(dom g)] & cod fg = [(cod f),(cod g)] ) by A4, Th38;
then ( dom f = c & cod f = c' & dom g = d & cod g = d' ) by A2, ZFMISC_1:33;
then ( f in Hom c,c' & g in Hom d,d' ) ;
hence x in [:(Hom c,c'),(Hom d,d'):] by A4, 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
A5: ( x1 in Hom c,c' & x2 in Hom d,d' ) and
A6: x = [x1,x2] by ZFMISC_1:def 2;
reconsider f = x1 as Morphism of c,c' by A5, CAT_1:def 7;
reconsider g = x2 as Morphism of d,d' by A5, CAT_1:def 7;
( dom f = c & cod f = c' & dom g = d & cod g = d' ) by A5, CAT_1:18;
then ( dom [f,g] = [c,d] & cod [f,g] = [c',d'] ) by Th38;
hence x in Hom [c,d],[c',d'] by A6; :: thesis: verum

end;

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