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