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 A1: ( F1,F2 are_naturally_equivalent & G1,G2 are_naturally_equivalent ) ; :: thesis: ( G1 * F1,G2 * F2 are_naturally_equivalent & f (#) e is natural_equivalence of G1 * F1,G2 * F2 )
then A2: ( F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 ) by Def4;
A3: ( G1 * F2,G2 * F2 are_naturally_equivalent & G1 * F1,G1 * F2 are_naturally_equivalent ) by A1, Th35, Th36;
then A4: ( G1 * F2 is_naturally_transformable_to G2 * F2 & G1 * F1 is_naturally_transformable_to G1 * F2 ) by Def4;
A5: ( f * F2 is natural_equivalence of G1 * F2,G2 * F2 & G1 * e is natural_equivalence of G1 * F1,G1 * F2 ) by A1, Th35, Th36;
reconsider sF2 = f * F2 as natural_transformation of G1 * F2,G2 * F2 by A2, Th29;
reconsider G1t = G1 * e as natural_transformation of G1 * F1,G1 * F2 by A2, Th28;
sF2 `*` G1t is natural_equivalence of G1 * F1,G2 * F2 by A3, A5, Th34;
hence ( G1 * F1,G2 * F2 are_naturally_equivalent & f (#) e is natural_equivalence of G1 * F1,G2 * F2 ) by A3, A4, Th33, FUNCTOR2:def 8; :: thesis: verum