let A, B, C be category; :: thesis: for F1, F2 being covariant Functor of A,B

for G1, G2 being covariant Functor of B,C

for e being natural_equivalence of F1,F2

for f being natural_equivalence of G1,G2 st F1,F2 are_naturally_equivalent & G1,G2 are_naturally_equivalent holds

( G1 * F1,G2 * F2 are_naturally_equivalent & f (#) e is natural_equivalence of G1 * F1,G2 * F2 )

let F1, F2 be covariant Functor of A,B; :: thesis: for G1, G2 being covariant Functor of B,C

for e being natural_equivalence of F1,F2

for f being natural_equivalence of G1,G2 st F1,F2 are_naturally_equivalent & G1,G2 are_naturally_equivalent holds

( G1 * F1,G2 * F2 are_naturally_equivalent & f (#) e is natural_equivalence of G1 * F1,G2 * F2 )

let G1, G2 be covariant Functor of B,C; :: thesis: for e being natural_equivalence of F1,F2

for f being natural_equivalence of G1,G2 st F1,F2 are_naturally_equivalent & G1,G2 are_naturally_equivalent holds

( G1 * F1,G2 * F2 are_naturally_equivalent & f (#) e is natural_equivalence of G1 * F1,G2 * F2 )

let e be natural_equivalence of F1,F2; :: thesis: for f being natural_equivalence of G1,G2 st F1,F2 are_naturally_equivalent & G1,G2 are_naturally_equivalent holds

( G1 * F1,G2 * F2 are_naturally_equivalent & f (#) e is natural_equivalence of G1 * F1,G2 * F2 )

let f be natural_equivalence of G1,G2; :: thesis: ( F1,F2 are_naturally_equivalent & G1,G2 are_naturally_equivalent implies ( G1 * F1,G2 * F2 are_naturally_equivalent & f (#) e is natural_equivalence of G1 * F1,G2 * F2 ) )

assume that

A1: F1,F2 are_naturally_equivalent and

A2: G1,G2 are_naturally_equivalent ; :: thesis: ( G1 * F1,G2 * F2 are_naturally_equivalent & f (#) e is natural_equivalence of G1 * F1,G2 * F2 )

A3: G1 * F1,G1 * F2 are_naturally_equivalent by A1, Th35;

G1 is_naturally_transformable_to G2 by A2;

then reconsider sF2 = f * F2 as natural_transformation of G1 * F2,G2 * F2 by Th29;

F1 is_naturally_transformable_to F2 by A1;

then reconsider G1t = G1 * e as natural_transformation of G1 * F1,G1 * F2 by Th28;

A4: G1 * F2,G2 * F2 are_naturally_equivalent by A2, Th36;

( f * F2 is natural_equivalence of G1 * F2,G2 * F2 & G1 * e is natural_equivalence of G1 * F1,G1 * F2 ) by A1, A2, Th35, Th36;

then sF2 `*` G1t is natural_equivalence of G1 * F1,G2 * F2 by A4, A3, Th34;

hence ( G1 * F1,G2 * F2 are_naturally_equivalent & f (#) e is natural_equivalence of G1 * F1,G2 * F2 ) by A4, A3, Th33, FUNCTOR2:def 8; :: thesis: verum

for G1, G2 being covariant Functor of B,C

for e being natural_equivalence of F1,F2

for f being natural_equivalence of G1,G2 st F1,F2 are_naturally_equivalent & G1,G2 are_naturally_equivalent holds

( G1 * F1,G2 * F2 are_naturally_equivalent & f (#) e is natural_equivalence of G1 * F1,G2 * F2 )

let F1, F2 be covariant Functor of A,B; :: thesis: for G1, G2 being covariant Functor of B,C

for e being natural_equivalence of F1,F2

for f being natural_equivalence of G1,G2 st F1,F2 are_naturally_equivalent & G1,G2 are_naturally_equivalent holds

( G1 * F1,G2 * F2 are_naturally_equivalent & f (#) e is natural_equivalence of G1 * F1,G2 * F2 )

let G1, G2 be covariant Functor of B,C; :: thesis: for e being natural_equivalence of F1,F2

for f being natural_equivalence of G1,G2 st F1,F2 are_naturally_equivalent & G1,G2 are_naturally_equivalent holds

( G1 * F1,G2 * F2 are_naturally_equivalent & f (#) e is natural_equivalence of G1 * F1,G2 * F2 )

let e be natural_equivalence of F1,F2; :: thesis: for f being natural_equivalence of G1,G2 st F1,F2 are_naturally_equivalent & G1,G2 are_naturally_equivalent holds

( G1 * F1,G2 * F2 are_naturally_equivalent & f (#) e is natural_equivalence of G1 * F1,G2 * F2 )

let f be natural_equivalence of G1,G2; :: thesis: ( F1,F2 are_naturally_equivalent & G1,G2 are_naturally_equivalent implies ( G1 * F1,G2 * F2 are_naturally_equivalent & f (#) e is natural_equivalence of G1 * F1,G2 * F2 ) )

assume that

A1: F1,F2 are_naturally_equivalent and

A2: G1,G2 are_naturally_equivalent ; :: thesis: ( G1 * F1,G2 * F2 are_naturally_equivalent & f (#) e is natural_equivalence of G1 * F1,G2 * F2 )

A3: G1 * F1,G1 * F2 are_naturally_equivalent by A1, Th35;

G1 is_naturally_transformable_to G2 by A2;

then reconsider sF2 = f * F2 as natural_transformation of G1 * F2,G2 * F2 by Th29;

F1 is_naturally_transformable_to F2 by A1;

then reconsider G1t = G1 * e as natural_transformation of G1 * F1,G1 * F2 by Th28;

A4: G1 * F2,G2 * F2 are_naturally_equivalent by A2, Th36;

( f * F2 is natural_equivalence of G1 * F2,G2 * F2 & G1 * e is natural_equivalence of G1 * F1,G1 * F2 ) by A1, A2, Th35, Th36;

then sF2 `*` G1t is natural_equivalence of G1 * F1,G2 * F2 by A4, A3, Th34;

hence ( G1 * F1,G2 * F2 are_naturally_equivalent & f (#) e is natural_equivalence of G1 * F1,G2 * F2 ) by A4, A3, Th33, FUNCTOR2:def 8; :: thesis: verum