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 ;
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
.= cod f by ;
A4: dom (f opp) = b opp by
.= cod f by ;
A5: cod (g opp) = b opp by
.= dom g by ;
A6: S . (f opp) = S . (f opp) by
.= (/* S) . f by Def8 ;
A7: S . (g opp) = S . (g opp) by
.= (/* S) . g by Def8 ;
thus (/* S) . (g (*) f) = S . ((g (*) f) opp) by Def8
.= S . ((f opp) (*) (g opp)) by
.= ((/* S) . f) (*) ((/* S) . g) by A7, A6, A5, A3, A4, CAT_1:64 ; :: thesis: verum