let A, B, C, D be Category; :: thesis: for F being Functor of A,B
for G being Functor of C,D
for I, J being Functor of B,C st I ~= J holds
( G * I ~= G * J & I * F ~= J * F )
let F be Functor of A,B; :: thesis: for G being Functor of C,D
for I, J being Functor of B,C st I ~= J holds
( G * I ~= G * J & I * F ~= J * F )
let G be Functor of C,D; :: thesis: for I, J being Functor of B,C st I ~= J holds
( G * I ~= G * J & I * F ~= J * F )
let I, J be Functor of B,C; :: thesis: ( I ~= J implies ( G * I ~= G * J & I * F ~= J * F ) )
assume A1: I is_naturally_transformable_to J ; :: according to NATTRA_1:def 11 :: thesis: ( for b₁ being natural_transformation of I,J holds not b₁ is invertible or ( G * I ~= G * J & I * F ~= J * F ) )
given t being natural_transformation of I,J such that A2: t is invertible ; :: thesis: ( G * I ~= G * J & I * F ~= J * F )
thus G * I ~= G * J :: thesis: I * F ~= J * F

proof

thus G * I is_naturally_transformable_to G * J by A1, Th20; :: according to NATTRA_1:def 11 :: thesis: ex b₁ being natural_transformation of G * I,G * J st b₁ is invertible
take G * t ; :: thesis: G * t is invertible
let b be Object of B; :: according to NATTRA_1:def 10 :: thesis: (G * t) . b is invertible
A3: t . b is invertible by A2;
A4: ( G . (I . b) = (G * I) . b & G . (J . b) = (G * J) . b ) by CAT_1:76;
(G * t) . b = G /. (t . b) by A1, Th21;
hence (G * t) . b is invertible by A3, Th1, A4; :: thesis: verum

end;

thus I * F is_naturally_transformable_to J * F by A1, Th20; :: according to NATTRA_1:def 11 :: thesis: ex b₁ being natural_transformation of I * F,J * F st b₁ is invertible
take t * F ; :: thesis: t * F is invertible
let a be Object of A; :: according to NATTRA_1:def 10 :: thesis: (t * F) . a is invertible
A5: ( I . (F . a) = (I * F) . a & J . (F . a) = (J * F) . a ) by CAT_1:76;
(t * F) . a = t . (F . a) by A1, Th22;
hence (t * F) . a is invertible by A2, A5; :: thesis: verum