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

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