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
A1: F1 is_transformable_to F2 and
A2: 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)) <> {}
A3: t . a is invertible by A2;
Hom ((F1 . a),(F2 . a)) <> {} by A1, Def2;
hence Hom ((F2 . a),(F1 . a)) <> {} by A3, CAT_1:41; :: thesis: verum