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 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 Def11
.= (T . (S . f)) opp by FUNCT_2:15
.= (T *') . (S . f) by Def11
.= ((T *') * S) . f by FUNCT_2:15 ; :: thesis: verum

end;

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