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

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

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

proof

let c9 be Object of C9; :: thesis: ex d being Object of D st T . (id c9) = id d
consider d being Object of D such that
A1: S . (id [c,c9]) = id d by CAT_1:62;
take d ; :: thesis: T . (id c9) = id d
thus T . (id c9) = S . ((id c),(id c9)) by FUNCT_5:69
.= id d by A1, Th25 ; :: thesis: verum

end;

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

proof

let f be Morphism of C9; :: 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 FUNCT_5:69
.= S . (id [c,(dom f)]) by Th25
.= S . (id [(dom (id c)),(dom f)])
.= S . (id (dom [(id c),f])) by Th22
.= id (dom (S . ((id c),f))) by CAT_1:63
.= id (dom (T . f)) by FUNCT_5:69 ; :: thesis: T . (id (cod f)) = id (cod (T . f))
thus T . (id (cod f)) = S . ((id c),(id (cod f))) by FUNCT_5:69
.= S . (id [c,(cod f)]) by Th25
.= S . (id [(cod (id c)),(cod f)])
.= S . (id (cod [(id c),f])) by Th22
.= id (cod (S . ((id c),f))) by CAT_1:63
.= id (cod (T . f)) by FUNCT_5:69 ; :: thesis: verum

end;

let f, g be Morphism of C9; :: 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) <> {} ;
then A4: (id c) * (id c) = (id c) (*) (id c) by CAT_1:def 13;
A5: ( dom [(id c),g] = [(dom (id c)),(dom g)] & cod [(id c),f] = [(cod (id c)),(cod f)] ) by Th22;
thus T . (g (*) f) = S . (((id c) * (id c)),(g (*) f)) by FUNCT_5:69
.= S . ([(id c),g] (*) [(id c),f]) by A3, A2, A4, Th23
.= (S . ((id c),g)) (*) (S . ((id c),f)) by A3, A5, CAT_1:64
.= (T . g) (*) (S . ((id c),f)) by FUNCT_5:69
.= (T . g) (*) (T . f) by FUNCT_5:69 ; :: thesis: verum

end;

hence (curry S) . (id c) is Functor of C9,D by CAT_1:61; :: thesis: verum