let C, C', D be Category; :: thesis: for S being Functor of [:C,C':],D
for c being Object of C holds (curry S) . (id c) is Functor of C',D
let S be Functor of [:C,C':],D; :: thesis: for c being Object of C holds (curry S) . (id c) is Functor of C',D
let c be Object of C; :: 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 C' ex d being Object of D st T . (id c') = id d :: thesis: ( ( 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 c' be Object of C'; :: thesis: ex d being Object of D st T . (id c') = id d
consider d being Object of D 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 Th3
.= id d by A1, Th41 ; :: thesis: verum

end;

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

end;

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

end;

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