let A, B, C be category; :: thesis: for F1, F2 being covariant Functor of A,B
for G1, G2 being covariant Functor of B,C
for e being natural_equivalence of F1,F2
for f being natural_equivalence of G1,G2 st F1,F2 are_naturally_equivalent & G1,G2 are_naturally_equivalent holds
( G1 * F1,G2 * F2 are_naturally_equivalent & f (#) e is natural_equivalence of G1 * F1,G2 * F2 )
let F1, F2 be covariant Functor of A,B; :: thesis: for G1, G2 being covariant Functor of B,C
for e being natural_equivalence of F1,F2
for f being natural_equivalence of G1,G2 st F1,F2 are_naturally_equivalent & G1,G2 are_naturally_equivalent holds
( G1 * F1,G2 * F2 are_naturally_equivalent & f (#) e is natural_equivalence of G1 * F1,G2 * F2 )
let G1, G2 be covariant Functor of B,C; :: thesis: for e being natural_equivalence of F1,F2
for f being natural_equivalence of G1,G2 st F1,F2 are_naturally_equivalent & G1,G2 are_naturally_equivalent holds
( G1 * F1,G2 * F2 are_naturally_equivalent & f (#) e is natural_equivalence of G1 * F1,G2 * F2 )
let e be natural_equivalence of F1,F2; :: thesis: for f being natural_equivalence of G1,G2 st F1,F2 are_naturally_equivalent & G1,G2 are_naturally_equivalent holds
( G1 * F1,G2 * F2 are_naturally_equivalent & f (#) e is natural_equivalence of G1 * F1,G2 * F2 )
let f be natural_equivalence of G1,G2; :: thesis: ( F1,F2 are_naturally_equivalent & G1,G2 are_naturally_equivalent implies ( G1 * F1,G2 * F2 are_naturally_equivalent & f (#) e is natural_equivalence of G1 * F1,G2 * F2 ) )
assume that
A1: F1,F2 are_naturally_equivalent and
A2: G1,G2 are_naturally_equivalent ; :: thesis: ( G1 * F1,G2 * F2 are_naturally_equivalent & f (#) e is natural_equivalence of G1 * F1,G2 * F2 )
A3: G1 * F1,G1 * F2 are_naturally_equivalent by A1, Th35;
then A4: G1 * F1 is_naturally_transformable_to G1 * F2 by Def4;
G1 is_naturally_transformable_to G2 by A2, Def4;
then reconsider sF2 = f * F2 as natural_transformation of G1 * F2,G2 * F2 by Th29;
F1 is_naturally_transformable_to F2 by A1, Def4;
then reconsider G1t = G1 * e as natural_transformation of G1 * F1,G1 * F2 by Th28;
A5: G1 * F2,G2 * F2 are_naturally_equivalent by A2, Th36;
then A6: G1 * F2 is_naturally_transformable_to G2 * F2 by Def4;
( f * F2 is natural_equivalence of G1 * F2,G2 * F2 & G1 * e is natural_equivalence of G1 * F1,G1 * F2 ) by A1, A2, Th35, Th36;
then sF2 `*` G1t is natural_equivalence of G1 * F1,G2 * F2 by A5, A3, Th34;
hence ( G1 * F1,G2 * F2 are_naturally_equivalent & f (#) e is natural_equivalence of G1 * F1,G2 * F2 ) by A5, A3, A6, A4, Th33, FUNCTOR2:def 8; :: thesis: verum