let B, C, D be Category; :: thesis: for F1 being Function of the carrier' of C, the carrier' of B
for F2 being Function of the carrier' of B, the carrier' of D holds (*' (F2 * F1)) *' = ((*' F2) *') * ((*' F1) *')
let F1 be Function of the carrier' of C, the carrier' of B; :: thesis: for F2 being Function of the carrier' of B, the carrier' of D holds (*' (F2 * F1)) *' = ((*' F2) *') * ((*' F1) *')
let F2 be Function of the carrier' of B, the carrier' of D; :: thesis: (*' (F2 * F1)) *' = ((*' F2) *') * ((*' F1) *')

now :: thesis: for f being Morphism of (C opp) holds ((*' (F2 * F1)) *') . f = (((*' F2) *') * ((*' F1) *')) . f

let f be Morphism of (C opp); :: thesis: ((*' (F2 * F1)) *') . f = (((*' F2) *') * ((*' F1) *')) . f
thus ((*' (F2 * F1)) *') . f = ((F2 * F1) . (opp f)) opp by Lm17
.= (F2 . (F1 . (opp f))) opp by FUNCT_2:15
.= ((*' F2) *') . ((F1 . (opp f)) opp) by Th44
.= ((*' F2) *') . (((*' F1) *') . f) by Lm17
.= (((*' F2) *') * ((*' F1) *')) . f by FUNCT_2:15 ; :: thesis: verum

end;

hence (*' (F2 * F1)) *' = ((*' F2) *') * ((*' F1) *') by FUNCT_2:63; :: thesis: verum