let A, B, C be category; 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; 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; 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; ( 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
; ( 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;
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; verum