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) *')

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

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