let C, D, C9 be Category; :: thesis: 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; :: thesis: for c9 being Object of C9 holds (curry' S) . (id c9) is Functor of C,D

let c9 be Object of C9; :: thesis: (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 ;

for c9 being Object of C9 holds (curry' S) . (id c9) is Functor of C,D

let S be Functor of [:C,C9:],D; :: thesis: for c9 being Object of C9 holds (curry' S) . (id c9) is Functor of C,D

let c9 be Object of C9; :: thesis: (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 :: thesis: ( ( 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) ) )

hence
(curry' S) . (id c9) is Functor of C,D
by CAT_1:61; :: thesis: verum( 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
:: 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) ) )

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)

assume A3: dom g = cod f ; :: thesis: 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 ; :: thesis: verum

end;( 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

A2:
( dom (id c9) = c9 & cod (id c9) = c9 )
;
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,c9]) = id d by CAT_1:62;

take d ; :: thesis: T . (id c) = id d

thus T . (id c) = S . ((id c),(id c9)) by FUNCT_5:70

.= id d by A1, Th25 ; :: thesis: verum

end;consider d being Object of D such that

A1: S . (id [c,c9]) = id d by CAT_1:62;

take d ; :: thesis: T . (id c) = id d

thus T . (id c) = S . ((id c),(id c9)) by FUNCT_5:70

.= id d by A1, Th25 ; :: thesis: verum

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, g be Morphism of C; :: thesis: ( dom g = cod f implies T . (g (*) f) = (T . g) (*) (T . f) )
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 (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 ; :: thesis: 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 ; :: thesis: verum

end;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 ; :: thesis: 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 ; :: thesis: verum

assume A3: dom g = cod f ; :: thesis: 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 ; :: thesis: verum