let A, B be Category; for F1, F2 being Functor of A,B
for t1 being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 & t1 is invertible holds
for a being Object of A holds (t1 ") . a = (t1 . a) "
let F1, F2 be Functor of A,B; for t1 being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 & t1 is invertible holds
for a being Object of A holds (t1 ") . a = (t1 . a) "
let t1 be natural_transformation of F1,F2; ( F1 is_naturally_transformable_to F2 & t1 is invertible implies for a being Object of A holds (t1 ") . a = (t1 . a) " )
assume that
A1:
F1 is_naturally_transformable_to F2
and
A2:
t1 is invertible
; for a being Object of A holds (t1 ") . a = (t1 . a) "
let a be Object of A; (t1 ") . a = (t1 . a) "
A3:
F1 is_transformable_to F2
by A1;
thus (t1 ") . a =
(t1 ") . a
by A1, A2, Def12
.=
(t1 . a) "
by A2, A3, Def11
; verum