let C, D be Category; 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; 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; Hom ([c,d],[c9,d9]) = [:(Hom (c,c9)),(Hom (d,d9)):]
now 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 ;
( ( 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)):] )
( 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])
;
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;
verum
end; assume
x in [:(Hom (c,c9)),(Hom (d,d9)):]
;
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;
verum end;
hence
Hom ([c,d],[c9,d9]) = [:(Hom (c,c9)),(Hom (d,d9)):]
by TARSKI:2; verum