reconsider T = pr1 ( the carrier' of C, the carrier' of D) as Function of the carrier' of [:C,D:], the carrier' of C ;
now ( ( for cd being Object of [:C,D:] ex c being Object of C st T . (id cd) = id c ) & ( for fg being Morphism of [:C,D:] holds
( T . (id (dom fg)) = id (dom (T . fg)) & T . (id (cod fg)) = id (cod (T . fg)) ) ) & ( for fg, fg9 being Morphism of [:C,D:] st dom fg9 = cod fg holds
T . (fg9 (*) fg) = (T . fg9) (*) (T . fg) ) )thus
for
cd being
Object of
[:C,D:] ex
c being
Object of
C st
T . (id cd) = id c
( ( for fg being Morphism of [:C,D:] holds
( T . (id (dom fg)) = id (dom (T . fg)) & T . (id (cod fg)) = id (cod (T . fg)) ) ) & ( for fg, fg9 being Morphism of [:C,D:] st dom fg9 = cod fg holds
T . (fg9 (*) fg) = (T . fg9) (*) (T . fg) ) )thus
for
fg being
Morphism of
[:C,D:] holds
(
T . (id (dom fg)) = id (dom (T . fg)) &
T . (id (cod fg)) = id (cod (T . fg)) )
for fg, fg9 being Morphism of [:C,D:] st dom fg9 = cod fg holds
T . (fg9 (*) fg) = (T . fg9) (*) (T . fg)proof
let fg be
Morphism of
[:C,D:];
( T . (id (dom fg)) = id (dom (T . fg)) & T . (id (cod fg)) = id (cod (T . fg)) )
consider f being
Morphism of
C,
g being
Morphism of
D such that A3:
fg = [f,g]
by DOMAIN_1:1;
T . (
f,
g)
= T . fg
by A3;
then A4:
T . fg = f
by FUNCT_3:def 4;
dom [f,g] = [(dom f),(dom g)]
by Th22;
hence T . (id (dom fg)) =
T . (
(id (dom f)),
(id (dom g)))
by A3, Th25
.=
id (dom (T . fg))
by A4, FUNCT_3:def 4
;
T . (id (cod fg)) = id (cod (T . fg))
cod [f,g] = [(cod f),(cod g)]
by Th22;
hence T . (id (cod fg)) =
T . (
(id (cod f)),
(id (cod g)))
by A3, Th25
.=
id (cod (T . fg))
by A4, FUNCT_3:def 4
;
verum
end; let fg,
fg9 be
Morphism of
[:C,D:];
( dom fg9 = cod fg implies T . (fg9 (*) fg) = (T . fg9) (*) (T . fg) )assume A5:
dom fg9 = cod fg
;
T . (fg9 (*) fg) = (T . fg9) (*) (T . fg)consider f being
Morphism of
C,
g being
Morphism of
D such that A6:
fg = [f,g]
by DOMAIN_1:1;
T . (
f,
g)
= T . fg
by A6;
then A7:
T . fg = f
by FUNCT_3:def 4;
consider f9 being
Morphism of
C,
g9 being
Morphism of
D such that A8:
fg9 = [f9,g9]
by DOMAIN_1:1;
T . (
f9,
g9)
= T . fg9
by A8;
then A9:
T . fg9 = f9
by FUNCT_3:def 4;
(
dom [f9,g9] = [(dom f9),(dom g9)] &
cod [f,g] = [(cod f),(cod g)] )
by Th22;
then
(
dom f9 = cod f &
dom g9 = cod g )
by A5, A6, A8, XTUPLE_0:1;
hence T . (fg9 (*) fg) =
T . (
(f9 (*) f),
(g9 (*) g))
by A6, A8, Th23
.=
(T . fg9) (*) (T . fg)
by A9, A7, FUNCT_3:def 4
;
verum end;
hence
pr1 ( the carrier' of C, the carrier' of D) is Functor of [:C,D:],C
by CAT_1:61; verum