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