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, Th27; :: 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
I is_transformable_to J by A1, NATTRA_1:def 7;
then A3: Hom (I . b),(J . b) <> {} by NATTRA_1:def 2;
A4: (G * t) . b = G . (t . b) by A1, Th28
.= G . (t . b) by A3, NATTRA_1:def 1 ;
t . b is invertible by A2, NATTRA_1:def 10;
hence (G * t) . b is invertible by A4, Th3; :: thesis: verum

end;

thus I * F is_naturally_transformable_to J * F by A1, Th27; :: 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
(t * F) . a = t . (F . a) by A1, Th29;
hence (t * F) . a is invertible by A2, NATTRA_1:def 10; :: thesis: verum