let B, C, D be Category; :: thesis: for S being Function of the carrier' of (C opp), the carrier' of B
for T being Function of the carrier' of B, the carrier' of D holds /* (T * S) = T * (/* S)
let S be Function of the carrier' of (C opp), the carrier' of B; :: thesis: for T being Function of the carrier' of B, the carrier' of D holds /* (T * S) = T * (/* S)
let T be Function of the carrier' of B, the carrier' of D; :: thesis: /* (T * S) = T * (/* S)

now :: thesis: for f being Morphism of C holds (/* (T * S)) . f = (T * (/* S)) . f

let f be Morphism of C; :: thesis: (/* (T * S)) . f = (T * (/* S)) . f
thus (/* (T * S)) . f = (T * S) . (f opp) by Def8
.= T . (S . (f opp)) by FUNCT_2:15
.= T . ((/* S) . f) by Def8
.= (T * (/* S)) . f by FUNCT_2:15 ; :: thesis: verum

end;

hence /* (T * S) = T * (/* S) by FUNCT_2:63; :: thesis: verum