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)):]

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]) ) )

hence
Hom ([c,d],[c9,d9]) = [:(Hom (c,c9)),(Hom (d,d9)):]
by TARSKI:2; :: thesis: verum( ( 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]) )

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;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
x in [:(Hom (c,c9)),(Hom (d,d9)):]
; :: thesis: x in Hom ([c,d],[c9,d9])
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;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

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