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 t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds
G1 * t is natural_transformation of G1 * F1,G1 * F2
let F1, F2 be covariant Functor of A,B; :: thesis: for G1 being covariant Functor of B,C
for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds
G1 * t is natural_transformation of G1 * F1,G1 * F2
let G1 be covariant Functor of B,C; :: thesis: for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds
G1 * t is natural_transformation of G1 * F1,G1 * F2
let t be natural_transformation of F1,F2; :: thesis: ( F1 is_naturally_transformable_to F2 implies G1 * t is natural_transformation of G1 * F1,G1 * F2 )
assume A1: F1 is_naturally_transformable_to F2 ; :: thesis: G1 * t is natural_transformation of G1 * F1,G1 * F2
then A2: F1 is_transformable_to F2 ;
thus G1 * F1 is_naturally_transformable_to G1 * F2 by A1, Lm2; :: according to FUNCTOR2:def 7 :: thesis: for b₁, b₂ being M3( the carrier of A) holds
( <^b₁,b₂^> = {} or for b₃ being M3(<^b₁,b₂^>) holds ((G1 * t) ! b₂) * ((G1 * F1) . b₃) = ((G1 * F2) . b₃) * ((G1 * t) ! b₁) )
let a, b be Object of A; :: thesis: ( <^a,b^> = {} or for b₁ being M3(<^a,b^>) holds ((G1 * t) ! b) * ((G1 * F1) . b₁) = ((G1 * F2) . b₁) * ((G1 * t) ! a) )
assume A3: <^a,b^> <> {} ; :: thesis: for b₁ being M3(<^a,b^>) holds ((G1 * t) ! b) * ((G1 * F1) . b₁) = ((G1 * F2) . b₁) * ((G1 * t) ! a)
A4: ( (G1 * F1) . b = G1 . (F1 . b) & <^(F1 . a),(F1 . b)^> <> {} ) by A3, FUNCTOR0:33, FUNCTOR0:def 18;
A5: <^(F1 . b),(F2 . b)^> <> {} by A2;
A6: <^(F1 . a),(F2 . a)^> <> {} by A2;
reconsider G1ta = G1 . (t ! a) as Morphism of (G1 . (F1 . a)),((G1 * F2) . a) by FUNCTOR0:33;
reconsider G1tb = G1 . (t ! b) as Morphism of ((G1 * F1) . b),(G1 . (F2 . b)) by FUNCTOR0:33;
let f be Morphism of a,b; :: thesis: ((G1 * t) ! b) * ((G1 * F1) . f) = ((G1 * F2) . f) * ((G1 * t) ! a)
A7: (G1 * F2) . a = G1 . (F2 . a) by FUNCTOR0:33;
A8: <^(F2 . a),(F2 . b)^> <> {} by A3, FUNCTOR0:def 18;
A9: (G1 * F1) . a = G1 . (F1 . a) by FUNCTOR0:33;
then reconsider G1F1f = G1 . (F1 . f) as Morphism of ((G1 * F1) . a),((G1 * F1) . b) by FUNCTOR0:33;
A10: (G1 * F2) . b = G1 . (F2 . b) by FUNCTOR0:33;
hence ((G1 * t) ! b) * ((G1 * F1) . f) = G1tb * ((G1 * F1) . f) by A2, Th11
.= G1tb * G1F1f by A3, Th6
.= G1 . ((t ! b) * (F1 . f)) by A9, A4, A5, FUNCTOR0:def 23
.= G1 . ((F2 . f) * (t ! a)) by A1, A3, FUNCTOR2:def 7
.= (G1 . (F2 . f)) * (G1 . (t ! a)) by A6, A8, FUNCTOR0:def 23
.= ((G1 * F2) . f) * G1ta by A3, A7, A10, Th6
.= ((G1 * F2) . f) * ((G1 * t) ! a) by A2, A9, Th11 ;
:: thesis: verum