let A, B be Category; :: thesis: for F1, F2 being Functor of A,B
for t being transformation of F1,F2 st F1 is_transformable_to F2 & t is invertible holds
F2 is_transformable_to F1
let F1, F2 be Functor of A,B; :: thesis: for t being transformation of F1,F2 st F1 is_transformable_to F2 & t is invertible holds
F2 is_transformable_to F1
let t be transformation of F1,F2; :: thesis: ( F1 is_transformable_to F2 & t is invertible implies F2 is_transformable_to F1 )
assume that
F1 is_transformable_to F2 and
A1: for a being Object of A holds t . a is invertible ; :: according to NATTRA_1:def 10 :: thesis: F2 is_transformable_to F1
let a be Object of A; :: according to NATTRA_1:def 2 :: thesis: Hom ((F2 . a),(F1 . a)) <> {}
A2: t . a is invertible by A1;
thus Hom ((F2 . a),(F1 . a)) <> {} by A2; :: thesis: verum