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