let C, C', D be Category; :: thesis: for S being Functor of [:C,C':],D
for c' being Object of holds (curry' S) . (id c') is Functor of C,D
let S be Functor of [:C,C':],D; :: thesis: for c' being Object of holds (curry' S) . (id c') is Functor of C,D
let c' be Object of ; :: thesis: (curry' S) . (id c') is Functor of C,D
reconsider S' = S as Function of [:the carrier' of C,the carrier' of C':],the carrier' of D ;
reconsider T = (curry' S') . (id c') as Function of the carrier' of C,the carrier' of D ;

now

thus for c being Object of ex d being Object of st T . (id c) = id d :: thesis: ( ( for f being Morphism of holds
( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) ) ) & ( for f, g being Morphism of st dom g = cod f holds
T . (g * f) = (T . g) * (T . f) ) )

proof

let c be Object of ; :: thesis: ex d being Object of st T . (id c) = id d
consider d being Object of such that
A1: S . (id [c,c']) = id d by CAT_1:97;
take d ; :: thesis: T . (id c) = id d
thus T . (id c) = S . (id c),(id c') by Th4
.= id d by A1, Th41 ; :: thesis: verum

end;

A2: ( dom (id c') = c' & cod (id c') = c' ) by CAT_1:44;
thus for f being Morphism of holds
( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) ) :: thesis: for f, g being Morphism of st dom g = cod f holds
T . (g * f) = (T . g) * (T . f)

proof

let f be Morphism of ; :: thesis: ( 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 c') by Th4
.= S . (id [(dom f),c']) by Th41
.= S . (id [(dom f),(dom (id c'))]) by CAT_1:44
.= S . (id (dom [f,(id c')])) by Th38
.= id (dom (S . f,(id c'))) by CAT_1:98
.= id (dom (T . f)) by Th4 ; :: thesis: T . (id (cod f)) = id (cod (T . f))
thus T . (id (cod f)) = S . (id (cod f)),(id c') by Th4
.= S . (id [(cod f),c']) by Th41
.= S . (id [(cod f),(cod (id c'))]) by CAT_1:44
.= S . (id (cod [f,(id c')])) by Th38
.= id (cod (S . f,(id c'))) by CAT_1:98
.= id (cod (T . f)) by Th4 ; :: thesis: verum

end;

let f, g be Morphism of ; :: thesis: ( dom g = cod f implies T . (g * f) = (T . g) * (T . f) )
assume A3: dom g = cod f ; :: thesis: T . (g * f) = (T . g) * (T . f)
Hom c',c' <> {} by CAT_1:56;
then A4: (id c') * (id c') = (id c') * (id c') by CAT_1:def 13;
A5: ( dom [g,(id c')] = [(dom g),(dom (id c'))] & cod [f,(id c')] = [(cod f),(cod (id c'))] ) by Th38;
(id c') * (id c') = id c' by CAT_1:59;
hence T . (g * f) = S . (g * f),((id c') * (id c')) by Th4
.= S . ([g,(id c')] * [f,(id c')]) by A3, A2, A4, Th39
.= (S . g,(id c')) * (S . f,(id c')) by A3, A2, A5, CAT_1:99
.= (T . g) * (S . f,(id c')) by Th4
.= (T . g) * (T . f) by Th4 ;
:: thesis: verum

end;

hence (curry' S) . (id c') is Functor of C,D by CAT_1:96; :: thesis: verum