let B, C be Category; :: thesis: for S being Functor of C opp ,B

for a, b, c being Object of C st Hom (a,b) <> {} & Hom (b,c) <> {} holds

for f being Morphism of a,b

for g being Morphism of b,c holds (/* S) . (g (*) f) = ((/* S) . f) (*) ((/* S) . g)

let S be Functor of C opp ,B; :: thesis: for a, b, c being Object of C st Hom (a,b) <> {} & Hom (b,c) <> {} holds

for f being Morphism of a,b

for g being Morphism of b,c holds (/* S) . (g (*) f) = ((/* S) . f) (*) ((/* S) . g)

let a, b, c be Object of C; :: thesis: ( Hom (a,b) <> {} & Hom (b,c) <> {} implies for f being Morphism of a,b

for g being Morphism of b,c holds (/* S) . (g (*) f) = ((/* S) . f) (*) ((/* S) . g) )

assume A1: ( Hom (a,b) <> {} & Hom (b,c) <> {} ) ; :: thesis: for f being Morphism of a,b

for g being Morphism of b,c holds (/* S) . (g (*) f) = ((/* S) . f) (*) ((/* S) . g)

A2: ( Hom ((b opp),(a opp)) <> {} & Hom ((c opp),(b opp)) <> {} ) by A1, Th4;

let f be Morphism of a,b; :: thesis: for g being Morphism of b,c holds (/* S) . (g (*) f) = ((/* S) . f) (*) ((/* S) . g)

let g be Morphism of b,c; :: thesis: (/* S) . (g (*) f) = ((/* S) . f) (*) ((/* S) . g)

A3: dom g = b by A1, CAT_1:5

.= cod f by A1, CAT_1:5 ;

A4: dom (f opp) = b opp by A2, CAT_1:5

.= cod f by A1, CAT_1:5 ;

A5: cod (g opp) = b opp by A2, CAT_1:5

.= dom g by A1, CAT_1:5 ;

A6: S . (f opp) = S . (f opp) by A1, Def6

.= (/* S) . f by Def8 ;

A7: S . (g opp) = S . (g opp) by A1, Def6

.= (/* S) . g by Def8 ;

thus (/* S) . (g (*) f) = S . ((g (*) f) opp) by Def8

.= S . ((f opp) (*) (g opp)) by Th14, A1

.= ((/* S) . f) (*) ((/* S) . g) by A7, A6, A5, A3, A4, CAT_1:64 ; :: thesis: verum

for a, b, c being Object of C st Hom (a,b) <> {} & Hom (b,c) <> {} holds

for f being Morphism of a,b

for g being Morphism of b,c holds (/* S) . (g (*) f) = ((/* S) . f) (*) ((/* S) . g)

let S be Functor of C opp ,B; :: thesis: for a, b, c being Object of C st Hom (a,b) <> {} & Hom (b,c) <> {} holds

for f being Morphism of a,b

for g being Morphism of b,c holds (/* S) . (g (*) f) = ((/* S) . f) (*) ((/* S) . g)

let a, b, c be Object of C; :: thesis: ( Hom (a,b) <> {} & Hom (b,c) <> {} implies for f being Morphism of a,b

for g being Morphism of b,c holds (/* S) . (g (*) f) = ((/* S) . f) (*) ((/* S) . g) )

assume A1: ( Hom (a,b) <> {} & Hom (b,c) <> {} ) ; :: thesis: for f being Morphism of a,b

for g being Morphism of b,c holds (/* S) . (g (*) f) = ((/* S) . f) (*) ((/* S) . g)

A2: ( Hom ((b opp),(a opp)) <> {} & Hom ((c opp),(b opp)) <> {} ) by A1, Th4;

let f be Morphism of a,b; :: thesis: for g being Morphism of b,c holds (/* S) . (g (*) f) = ((/* S) . f) (*) ((/* S) . g)

let g be Morphism of b,c; :: thesis: (/* S) . (g (*) f) = ((/* S) . f) (*) ((/* S) . g)

A3: dom g = b by A1, CAT_1:5

.= cod f by A1, CAT_1:5 ;

A4: dom (f opp) = b opp by A2, CAT_1:5

.= cod f by A1, CAT_1:5 ;

A5: cod (g opp) = b opp by A2, CAT_1:5

.= dom g by A1, CAT_1:5 ;

A6: S . (f opp) = S . (f opp) by A1, Def6

.= (/* S) . f by Def8 ;

A7: S . (g opp) = S . (g opp) by A1, Def6

.= (/* S) . g by Def8 ;

thus (/* S) . (g (*) f) = S . ((g (*) f) opp) by Def8

.= S . ((f opp) (*) (g opp)) by Th14, A1

.= ((/* S) . f) (*) ((/* S) . g) by A7, A6, A5, A3, A4, CAT_1:64 ; :: thesis: verum