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