let A, B be Category; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: for a being Object of A holds (t1 ") . a = (t1 . a) "
let a be Object of A; :: thesis: (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 ; :: thesis: verum