let A, B, C 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: F2 is_transformable_to F1 ;

A3: F1 is_naturally_transformable_to F2 by A1;

then reconsider k = G1 * e as natural_transformation of G1 * F1,G1 * F2 by Th28;

A4: F1 is_transformable_to F2 by A1, Def4;

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

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: F2 is_transformable_to F1 ;

A3: F1 is_naturally_transformable_to F2 by A1;

then reconsider k = G1 * e as natural_transformation of G1 * F1,G1 * F2 by Th28;

A4: F1 is_transformable_to F2 by A1, Def4;

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

G1 * F1,G1 * F2 are_naturally_equivalent
by A3, Lm2, A2, Th10, A5;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:33;

A7: <^(F2 . a),(F1 . a)^> <> {} by A2;

( k ! a = G1 . (e ! a) & <^(F1 . a),(F2 . a)^> <> {} ) by A4, Th11;

hence k ! a is iso by A1, A6, A7, Def5, ALTCAT_4:20; :: thesis: verum

end;A6: ( (G1 * F1) . a = G1 . (F1 . a) & (G1 * F2) . a = G1 . (F2 . a) ) by FUNCTOR0:33;

A7: <^(F2 . a),(F1 . a)^> <> {} by A2;

( k ! a = G1 . (e ! a) & <^(F1 . a),(F2 . a)^> <> {} ) by A4, Th11;

hence k ! a is iso by A1, A6, A7, Def5, ALTCAT_4:20; :: thesis: verum

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