let C, B be Category; :: thesis: for S being Functor of C opp ,B
for f, g being Morphism of C st dom g = cod f holds
(/* S) . (g * f) = ((/* S) . f) * ((/* S) . g)
let S be Functor of C opp ,B; :: thesis: for f, g being Morphism of C st dom g = cod f holds
(/* S) . (g * f) = ((/* S) . f) * ((/* S) . g)
let f, g be Morphism of C; :: thesis: ( dom g = cod f implies (/* S) . (g * f) = ((/* S) . f) * ((/* S) . g) )
assume A1: dom g = cod f ; :: thesis: (/* S) . (g * f) = ((/* S) . f) * ((/* S) . g)
A2: ( dom (f opp) = cod f & cod (g opp) = dom g ) ;
thus (/* S) . (g * f) = S . ((g * f) opp) by Def6
.= S . ((f opp) * (g opp)) by A1, Th17
.= (S . (f opp)) * (S . (g opp)) by A1, A2, CAT_1:64
.= ((/* S) . f) * (S . (g opp)) by Def6
.= ((/* S) . f) * ((/* S) . g) by Def6 ; :: thesis: verum