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;

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

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 * F1,G2 * F1 are_naturally_equivalent by Lm2, A1, Th10, A2;
hence ( G1 * F1,G2 * F1 are_naturally_equivalent & f * F1 is natural_equivalence of G1 * F1,G2 * F1 ) by A2, Def5; :: thesis: verum