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 ;
A3: cod fg = [c9,d9] by ;
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 ;
then A8: cod f = c9 by ;
A9: cod g = d9 by ;
A10: dom fg = [(dom f),(dom g)] by ;
then dom g = d by ;
then A11: g in Hom (d,d9) by A9;
dom f = c by ;
then f in Hom (c,c9) by A8;
hence x in [:(Hom (c,c9)),(Hom (d,d9)):] by ; :: 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 ;
reconsider f = x1 as Morphism of c,c9 by ;
( cod f = c9 & cod g = d9 ) by ;
then A15: cod [f,g] = [c9,d9] by Th22;
( dom f = c & dom g = d ) by ;
then dom [f,g] = [c,d] by Th22;
hence x in Hom ([c,d],[c9,d9]) by ; :: thesis: verum
end;
hence Hom ([c,d],[c9,d9]) = [:(Hom (c,c9)),(Hom (d,d9)):] by TARSKI:2; :: thesis: verum