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

for G1, G2 being covariant Functor of B,C

for f being natural_equivalence of G1,G2 st G1,G2 are_naturally_equivalent holds

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

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

for f being natural_equivalence of G1,G2 st G1,G2 are_naturally_equivalent holds

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

let G1, G2 be covariant Functor of B,C; :: thesis: for f being natural_equivalence of G1,G2 st G1,G2 are_naturally_equivalent holds

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

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

assume A1: G1,G2 are_naturally_equivalent ; :: thesis: ( G1 * F1,G2 * F1 are_naturally_equivalent & f * F1 is natural_equivalence of G1 * F1,G2 * F1 )

then G1 is_naturally_transformable_to G2 ;

then reconsider k = f * F1 as natural_transformation of G1 * F1,G2 * F1 by Th29;

hence ( G1 * F1,G2 * F1 are_naturally_equivalent & f * F1 is natural_equivalence of G1 * F1,G2 * F1 ) by A2, Def5; :: thesis: verum

for G1, G2 being covariant Functor of B,C

for f being natural_equivalence of G1,G2 st G1,G2 are_naturally_equivalent holds

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

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

for f being natural_equivalence of G1,G2 st G1,G2 are_naturally_equivalent holds

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

let G1, G2 be covariant Functor of B,C; :: thesis: for f being natural_equivalence of G1,G2 st G1,G2 are_naturally_equivalent holds

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

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

assume A1: G1,G2 are_naturally_equivalent ; :: thesis: ( G1 * F1,G2 * F1 are_naturally_equivalent & f * F1 is natural_equivalence of G1 * F1,G2 * F1 )

then G1 is_naturally_transformable_to G2 ;

then reconsider k = f * F1 as natural_transformation of G1 * F1,G2 * F1 by Th29;

A2: now :: thesis: for a being Object of A holds k ! a is iso

G1 * F1,G2 * F1 are_naturally_equivalent
by Lm2, A1, Th10, A2;let a be Object of A; :: thesis: k ! a is iso

G1 is_transformable_to G2 by A1, Def4;

then A3: k ! a = f ! (F1 . a) by Th12;

( (G1 * F1) . a = G1 . (F1 . a) & (G2 * F1) . a = G2 . (F1 . a) ) by FUNCTOR0:33;

hence k ! a is iso by A1, A3, Def5; :: thesis: verum

end;G1 is_transformable_to G2 by A1, Def4;

then A3: k ! a = f ! (F1 . a) by Th12;

( (G1 * F1) . a = G1 . (F1 . a) & (G2 * F1) . a = G2 . (F1 . a) ) by FUNCTOR0:33;

hence k ! a is iso by A1, A3, Def5; :: thesis: verum

hence ( G1 * F1,G2 * F1 are_naturally_equivalent & f * F1 is natural_equivalence of G1 * F1,G2 * F1 ) by A2, Def5; :: thesis: verum