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 A2: G1 is_naturally_transformable_to G2 by Def4;
then reconsider k = f * F1 as natural_transformation of G1 * F1,G2 * F1 by Th29;

A3: now

let a be object of A; :: thesis: k ! a is iso
G1 is_transformable_to G2 by A1, Def4;
then A4: k ! a = f ! (F1 . a) by Th12;
( (G1 * F1) . a = G1 . (F1 . a) & (G2 * F1) . a = G2 . (F1 . a) ) by FUNCTOR0:34;
hence k ! a is iso by A1, A4, Def5; :: thesis: verum

end;

G1 * F1,G2 * F1 are_naturally_equivalent

proof

F1 is_naturally_transformable_to F1 by FUNCTOR2:9;
hence G1 * F1 is_naturally_transformable_to G2 * F1 by A2, Lm2; :: according to FUNCTOR3:def 4 :: thesis: ( G2 * F1 is_transformable_to G1 * F1 & ex t being natural_transformation of G1 * F1,G2 * F1 st
for a being object of A holds t ! a is iso )
G2 is_transformable_to G1 by A1, Def4;
hence G2 * F1 is_transformable_to G1 * F1 by Th10; :: thesis: ex t being natural_transformation of G1 * F1,G2 * F1 st
for a being object of A holds t ! a is iso
take k ; :: thesis: for a being object of A holds k ! a is iso
let a be object of A; :: thesis: k ! a is iso
thus k ! a is iso by A3; :: thesis: verum

end;

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