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
for o being Object of A st F1 is_transformable_to F2 holds
(G1 * p) ! o = G1 . (p ! o)
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
for o being Object of A st F1 is_transformable_to F2 holds
(G1 * p) ! o = G1 . (p ! o)
let G1 be covariant Functor of B,C; :: thesis: for p being transformation of F1,F2
for o being Object of A st F1 is_transformable_to F2 holds
(G1 * p) ! o = G1 . (p ! o)
let p be transformation of F1,F2; :: thesis: for o being Object of A st F1 is_transformable_to F2 holds
(G1 * p) ! o = G1 . (p ! o)
let o be Object of A; :: thesis: ( F1 is_transformable_to F2 implies (G1 * p) ! o = G1 . (p ! o) )
assume A1: F1 is_transformable_to F2 ; :: thesis: (G1 * p) ! o = G1 . (p ! o)
then G1 * F1 is_transformable_to G1 * F2 by Th10;
hence (G1 * p) ! o = (G1 * p) . o by FUNCTOR2:def 4
.= G1 . (p ! o) by A1, Def1 ;
:: thesis: verum