let C, A, B be category; :: thesis: for F1, F2 being covariant Functor of A,B
for G1 being covariant Functor of B,C
for e being natural_equivalence of F1,F2 st F1,F2 are_naturally_equivalent holds
( G1 * F1,G1 * F2 are_naturally_equivalent & G1 * e is natural_equivalence of G1 * F1,G1 * F2 )
let F1, F2 be covariant Functor of A,B; :: thesis: for G1 being covariant Functor of B,C
for e being natural_equivalence of F1,F2 st F1,F2 are_naturally_equivalent holds
( G1 * F1,G1 * F2 are_naturally_equivalent & G1 * e is natural_equivalence of G1 * F1,G1 * F2 )
let G1 be covariant Functor of B,C; :: thesis: for e being natural_equivalence of F1,F2 st F1,F2 are_naturally_equivalent holds
( G1 * F1,G1 * F2 are_naturally_equivalent & G1 * e is natural_equivalence of G1 * F1,G1 * F2 )
let e be natural_equivalence of F1,F2; :: thesis: ( F1,F2 are_naturally_equivalent implies ( G1 * F1,G1 * F2 are_naturally_equivalent & G1 * e is natural_equivalence of G1 * F1,G1 * F2 ) )
assume A1: F1,F2 are_naturally_equivalent ; :: thesis: ( G1 * F1,G1 * F2 are_naturally_equivalent & G1 * e is natural_equivalence of G1 * F1,G1 * F2 )
then A2: F1 is_naturally_transformable_to F2 by Def4;
A3: F1 is_transformable_to F2 by A1, Def4;
A4: F2 is_transformable_to F1 by A1, Def4;
reconsider k = G1 * e as natural_transformation of G1 * F1,G1 * F2 by A2, Th28;

A5: now

let a be object of A; :: thesis: k ! a is iso
A6: ( (G1 * F1) . a = G1 . (F1 . a) & (G1 * F2) . a = G1 . (F2 . a) ) by FUNCTOR0:34;
A7: k ! a = G1 . (e ! a) by A3, Th11;
A8: ( <^(F1 . a),(F2 . a)^> <> {} & <^(F2 . a),(F1 . a)^> <> {} ) by A3, A4, FUNCTOR2:def 1;
e ! a is iso by A1, Def5;
hence k ! a is iso by A6, A7, A8, ALTCAT_4:20; :: thesis: verum

end;

G1 * F1,G1 * F2 are_naturally_equivalent

proof

G1 is_naturally_transformable_to G1 by FUNCTOR2:9;
hence G1 * F1 is_naturally_transformable_to G1 * F2 by A2, Lm2; :: according to FUNCTOR3:def 4 :: thesis: ( G1 * F2 is_transformable_to G1 * F1 & ex t being natural_transformation of G1 * F1,G1 * F2 st
for a being object of A holds t ! a is iso )
thus G1 * F2 is_transformable_to G1 * F1 by A4, Th10; :: thesis: ex t being natural_transformation of G1 * F1,G1 * F2 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 A5; :: thesis: verum

end;

hence ( G1 * F1,G1 * F2 are_naturally_equivalent & G1 * e is natural_equivalence of G1 * F1,G1 * F2 ) by A5, Def5; :: thesis: verum