let B, C, D be Category; :: thesis: for S1 being Contravariant_Functor of C,B

for S2 being Contravariant_Functor of B,D holds S2 * S1 is Functor of C,D

let S1 be Contravariant_Functor of C,B; :: thesis: for S2 being Contravariant_Functor of B,D holds S2 * S1 is Functor of C,D

let S2 be Contravariant_Functor of B,D; :: thesis: S2 * S1 is Functor of C,D

set T = S2 * S1;

for S2 being Contravariant_Functor of B,D holds S2 * S1 is Functor of C,D

let S1 be Contravariant_Functor of C,B; :: thesis: for S2 being Contravariant_Functor of B,D holds S2 * S1 is Functor of C,D

let S2 be Contravariant_Functor of B,D; :: thesis: S2 * S1 is Functor of C,D

set T = S2 * S1;

now :: thesis: ( ( for c being Object of C ex d being Object of D st (S2 * S1) . (id c) = id d ) & ( for f being Morphism of C holds

( (S2 * S1) . (id (dom f)) = id (dom ((S2 * S1) . f)) & (S2 * S1) . (id (cod f)) = id (cod ((S2 * S1) . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds

(S2 * S1) . (g (*) f) = ((S2 * S1) . g) (*) ((S2 * S1) . f) ) )

hence
S2 * S1 is Functor of C,D
by CAT_1:61; :: thesis: verum( (S2 * S1) . (id (dom f)) = id (dom ((S2 * S1) . f)) & (S2 * S1) . (id (cod f)) = id (cod ((S2 * S1) . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds

(S2 * S1) . (g (*) f) = ((S2 * S1) . g) (*) ((S2 * S1) . f) ) )

thus
for c being Object of C ex d being Object of D st (S2 * S1) . (id c) = id d
:: thesis: ( ( for f being Morphism of C holds

( (S2 * S1) . (id (dom f)) = id (dom ((S2 * S1) . f)) & (S2 * S1) . (id (cod f)) = id (cod ((S2 * S1) . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds

(S2 * S1) . (g (*) f) = ((S2 * S1) . g) (*) ((S2 * S1) . f) ) )

( (S2 * S1) . (id (dom f)) = id (dom ((S2 * S1) . f)) & (S2 * S1) . (id (cod f)) = id (cod ((S2 * S1) . f)) ) :: thesis: for f, g being Morphism of C st dom g = cod f holds

(S2 * S1) . (g (*) f) = ((S2 * S1) . g) (*) ((S2 * S1) . f)

assume A3: dom g = cod f ; :: thesis: (S2 * S1) . (g (*) f) = ((S2 * S1) . g) (*) ((S2 * S1) . f)

then A4: cod (S1 . g) = dom (S1 . f) by Th31;

thus (S2 * S1) . (g (*) f) = S2 . (S1 . (g (*) f)) by FUNCT_2:15

.= S2 . ((S1 . f) (*) (S1 . g)) by A3, Def9

.= (S2 . (S1 . g)) (*) (S2 . (S1 . f)) by A4, Def9

.= ((S2 * S1) . g) (*) (S2 . (S1 . f)) by FUNCT_2:15

.= ((S2 * S1) . g) (*) ((S2 * S1) . f) by FUNCT_2:15 ; :: thesis: verum

end;( (S2 * S1) . (id (dom f)) = id (dom ((S2 * S1) . f)) & (S2 * S1) . (id (cod f)) = id (cod ((S2 * S1) . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds

(S2 * S1) . (g (*) f) = ((S2 * S1) . g) (*) ((S2 * S1) . f) ) )

proof

thus
for f being Morphism of C holds
let c be Object of C; :: thesis: ex d being Object of D st (S2 * S1) . (id c) = id d

consider b being Object of B such that

A1: S1 . (id c) = id b by Def9;

consider d being Object of D such that

A2: S2 . (id b) = id d by Def9;

take d ; :: thesis: (S2 * S1) . (id c) = id d

thus (S2 * S1) . (id c) = id d by A1, A2, FUNCT_2:15; :: thesis: verum

end;consider b being Object of B such that

A1: S1 . (id c) = id b by Def9;

consider d being Object of D such that

A2: S2 . (id b) = id d by Def9;

take d ; :: thesis: (S2 * S1) . (id c) = id d

thus (S2 * S1) . (id c) = id d by A1, A2, FUNCT_2:15; :: thesis: verum

( (S2 * S1) . (id (dom f)) = id (dom ((S2 * S1) . f)) & (S2 * S1) . (id (cod f)) = id (cod ((S2 * S1) . f)) ) :: thesis: for f, g being Morphism of C st dom g = cod f holds

(S2 * S1) . (g (*) f) = ((S2 * S1) . g) (*) ((S2 * S1) . f)

proof

let f, g be Morphism of C; :: thesis: ( dom g = cod f implies (S2 * S1) . (g (*) f) = ((S2 * S1) . g) (*) ((S2 * S1) . f) )
let f be Morphism of C; :: thesis: ( (S2 * S1) . (id (dom f)) = id (dom ((S2 * S1) . f)) & (S2 * S1) . (id (cod f)) = id (cod ((S2 * S1) . f)) )

thus (S2 * S1) . (id (dom f)) = S2 . (S1 . (id (dom f))) by FUNCT_2:15

.= S2 . (id (cod (S1 . f))) by Def9

.= id (dom (S2 . (S1 . f))) by Def9

.= id (dom ((S2 * S1) . f)) by FUNCT_2:15 ; :: thesis: (S2 * S1) . (id (cod f)) = id (cod ((S2 * S1) . f))

thus (S2 * S1) . (id (cod f)) = S2 . (S1 . (id (cod f))) by FUNCT_2:15

.= S2 . (id (dom (S1 . f))) by Def9

.= id (cod (S2 . (S1 . f))) by Def9

.= id (cod ((S2 * S1) . f)) by FUNCT_2:15 ; :: thesis: verum

end;thus (S2 * S1) . (id (dom f)) = S2 . (S1 . (id (dom f))) by FUNCT_2:15

.= S2 . (id (cod (S1 . f))) by Def9

.= id (dom (S2 . (S1 . f))) by Def9

.= id (dom ((S2 * S1) . f)) by FUNCT_2:15 ; :: thesis: (S2 * S1) . (id (cod f)) = id (cod ((S2 * S1) . f))

thus (S2 * S1) . (id (cod f)) = S2 . (S1 . (id (cod f))) by FUNCT_2:15

.= S2 . (id (dom (S1 . f))) by Def9

.= id (cod (S2 . (S1 . f))) by Def9

.= id (cod ((S2 * S1) . f)) by FUNCT_2:15 ; :: thesis: verum

assume A3: dom g = cod f ; :: thesis: (S2 * S1) . (g (*) f) = ((S2 * S1) . g) (*) ((S2 * S1) . f)

then A4: cod (S1 . g) = dom (S1 . f) by Th31;

thus (S2 * S1) . (g (*) f) = S2 . (S1 . (g (*) f)) by FUNCT_2:15

.= S2 . ((S1 . f) (*) (S1 . g)) by A3, Def9

.= (S2 . (S1 . g)) (*) (S2 . (S1 . f)) by A4, Def9

.= ((S2 * S1) . g) (*) (S2 . (S1 . f)) by FUNCT_2:15

.= ((S2 * S1) . g) (*) ((S2 * S1) . f) by FUNCT_2:15 ; :: thesis: verum