let C, D, C9 be Category; for S being Functor of [:C,C9:],D
for c9 being Object of C9 holds (curry' S) . (id c9) is Functor of C,D
let S be Functor of [:C,C9:],D; for c9 being Object of C9 holds (curry' S) . (id c9) is Functor of C,D
let c9 be Object of C9; (curry' S) . (id c9) is Functor of C,D
reconsider S9 = S as Function of [: the carrier' of C, the carrier' of C9:], the carrier' of D ;
reconsider T = (curry' S9) . (id c9) as Function of the carrier' of C, the carrier' of D ;
now ( ( for c being Object of C ex d being Object of D st T . (id c) = id d ) & ( for f being Morphism of C holds
( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds
T . (g (*) f) = (T . g) (*) (T . f) ) )thus
for
c being
Object of
C ex
d being
Object of
D st
T . (id c) = id d
( ( for f being Morphism of C holds
( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds
T . (g (*) f) = (T . g) (*) (T . f) ) )A2:
(
dom (id c9) = c9 &
cod (id c9) = c9 )
;
thus
for
f being
Morphism of
C holds
(
T . (id (dom f)) = id (dom (T . f)) &
T . (id (cod f)) = id (cod (T . f)) )
for f, g being Morphism of C st dom g = cod f holds
T . (g (*) f) = (T . g) (*) (T . f)proof
let f be
Morphism of
C;
( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) )
thus T . (id (dom f)) =
S . (
(id (dom f)),
(id c9))
by FUNCT_5:70
.=
S . (id [(dom f),c9])
by Th25
.=
S . (id [(dom f),(dom (id c9))])
.=
S . (id (dom [f,(id c9)]))
by Th22
.=
id (dom (S . (f,(id c9))))
by CAT_1:63
.=
id (dom (T . f))
by FUNCT_5:70
;
T . (id (cod f)) = id (cod (T . f))
thus T . (id (cod f)) =
S . (
(id (cod f)),
(id c9))
by FUNCT_5:70
.=
S . (id [(cod f),c9])
by Th25
.=
S . (id [(cod f),(cod (id c9))])
.=
S . (id (cod [f,(id c9)]))
by Th22
.=
id (cod (S . (f,(id c9))))
by CAT_1:63
.=
id (cod (T . f))
by FUNCT_5:70
;
verum
end; let f,
g be
Morphism of
C;
( dom g = cod f implies T . (g (*) f) = (T . g) (*) (T . f) )assume A3:
dom g = cod f
;
T . (g (*) f) = (T . g) (*) (T . f)
Hom (
c9,
c9)
<> {}
;
then A4:
(id c9) * (id c9) = (id c9) (*) (id c9)
by CAT_1:def 13;
A5:
(
dom [g,(id c9)] = [(dom g),(dom (id c9))] &
cod [f,(id c9)] = [(cod f),(cod (id c9))] )
by Th22;
thus T . (g (*) f) =
S . (
(g (*) f),
((id c9) * (id c9)))
by FUNCT_5:70
.=
S . ([g,(id c9)] (*) [f,(id c9)])
by A3, A2, A4, Th23
.=
(S . (g,(id c9))) (*) (S . (f,(id c9)))
by A3, A5, CAT_1:64
.=
(T . g) (*) (S . (f,(id c9)))
by FUNCT_5:70
.=
(T . g) (*) (T . f)
by FUNCT_5:70
;
verum end;
hence
(curry' S) . (id c9) is Functor of C,D
by CAT_1:61; verum