A2: G1 is_transformable_to G2 by A1;
t * F is natural_transformation of G1 * F,G2 * F

proof

thus G1 * F is_naturally_transformable_to G2 * F by A1, Th20; :: according to NATTRA_1:def 8 :: thesis: for b₁, b₂ being M3( the carrier of A) holds
( Hom (b₁,b₂) = {} or for b₃ being Morphism of b₁,b₂ holds ((t * F) . b₂) * ((G1 * F) /. b₃) = ((G2 * F) /. b₃) * ((t * F) . b₁) )
then A3: G1 * F is_transformable_to G2 * F ;
let a, b be Object of A; :: thesis: ( Hom (a,b) = {} or for b₁ being Morphism of a,b holds ((t * F) . b) * ((G1 * F) /. b₁) = ((G2 * F) /. b₁) * ((t * F) . a) )
A4: Hom (((G1 * F) . b),((G2 * F) . b)) <> {} by A3;
A5: Hom (((G1 * F) . a),((G2 * F) . a)) <> {} by A3;
assume A6: Hom (a,b) <> {} ; :: thesis: for b₁ being Morphism of a,b holds ((t * F) . b) * ((G1 * F) /. b₁) = ((G2 * F) /. b₁) * ((t * F) . a)
then A7: Hom (((G2 * F) . a),((G2 * F) . b)) <> {} by CAT_1:84;
let f be Morphism of a,b; :: thesis: ((t * F) . b) * ((G1 * F) /. f) = ((G2 * F) /. f) * ((t * F) . a)
A8: Hom ((F . a),(F . b)) <> {} by A6, CAT_1:84;
then A9: Hom ((G1 . (F . a)),(G1 . (F . b))) <> {} by CAT_1:84;
A10: Hom ((G1 . (F . a)),(G2 . (F . a))) <> {} by A2;
A11: Hom ((G1 . (F . b)),(G2 . (F . b))) <> {} by A2;
A12: Hom ((G2 . (F . a)),(G2 . (F . b))) <> {} by A8, CAT_1:84;
Hom (((G1 * F) . a),((G1 * F) . b)) <> {} by A6, CAT_1:84;
hence ((t * F) . b) * ((G1 * F) /. f) = ((t * F) . b) (*) ((G1 * F) /. f) by A4, CAT_1:def 13
.= ((t * F) . b) (*) (G1 /. (F /. f)) by A6, NATTRA_1:11
.= (t . (F . b)) (*) (G1 /. (F /. f)) by A2, Th18
.= (t . (F . b)) * (G1 /. (F /. f)) by A11, A9, CAT_1:def 13
.= (G2 /. (F /. f)) * (t . (F . a)) by A1, A8, NATTRA_1:def 8
.= (G2 /. (F /. f)) (*) (t . (F . a)) by A12, A10, CAT_1:def 13
.= (G2 /. (F /. f)) (*) ((t * F) . a) by A2, Th18
.= ((G2 * F) /. f) (*) ((t * F) . a) by A6, NATTRA_1:11
.= ((G2 * F) /. f) * ((t * F) . a) by A7, A5, CAT_1:def 13 ;
:: thesis: verum

end;

hence t * F is natural_transformation of G1 * F,G2 * F ; :: thesis: verum