let A, B, C be non empty transitive with_units AltCatStr ; :: thesis: for F1, F2 being covariant Functor of A,B
for G1 being covariant Functor of B,C
for p being transformation of F1,F2 st F1 is_transformable_to F2 holds
G1 * p = (idt G1) (#) p
let F1, F2 be covariant Functor of A,B; :: thesis: for G1 being covariant Functor of B,C
for p being transformation of F1,F2 st F1 is_transformable_to F2 holds
G1 * p = (idt G1) (#) p
let G1 be covariant Functor of B,C; :: thesis: for p being transformation of F1,F2 st F1 is_transformable_to F2 holds
G1 * p = (idt G1) (#) p
let p be transformation of F1,F2; :: thesis: ( F1 is_transformable_to F2 implies G1 * p = (idt G1) (#) p )
assume F1 is_transformable_to F2 ; :: thesis: G1 * p = (idt G1) (#) p
then G1 * F1 is_transformable_to G1 * F2 by Th10;
hence G1 * p = (idt (G1 * F2)) `*` (G1 * p) by FUNCTOR2:5
.= (idt G1) (#) p by Th18 ;
:: thesis: verum