let B, C, D be Category; :: thesis: for S being Function of the carrier' of C, 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, 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 opp) holds (*' (T * S)) . f = (T * (*' S)) . f

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

end;

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