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

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

hence
(T * S) *' = (T *') * S
by FUNCT_2:63; :: thesis: verumlet 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;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