let C, B, 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

let f be Morphism of (C opp ); :: thesis: ((*' (F2 * F1)) *' ) . f = (((*' F2) *' ) * ((*' F1) *' )) . f
thus ((*' (F2 * F1)) *' ) . f = ((F2 * F1) . (opp f)) opp by Lm14
.= (F2 . (F1 . (opp f))) opp by FUNCT_2:21
.= ((*' F2) *' ) . ((F1 . (opp f)) opp ) by Th47
.= ((*' F2) *' ) . (((*' F1) *' ) . f) by Lm14
.= (((*' F2) *' ) * ((*' F1) *' )) . f by FUNCT_2:21 ; :: thesis: verum

end;

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