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
F2 is_naturally_transformable_to F1
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
F2 is_naturally_transformable_to F1
let t1 be natural_transformation of F1,F2; :: thesis: ( F1 is_naturally_transformable_to F2 & t1 is invertible implies F2 is_naturally_transformable_to F1 )
assume A1: F1 is_naturally_transformable_to F2 ; :: thesis: ( not t1 is invertible or F2 is_naturally_transformable_to F1 )
assume A2: t1 is invertible ; :: thesis: F2 is_naturally_transformable_to F1
hence F2 is_transformable_to F1 by A1, Lm3; :: according to NATTRA_1:def 7 :: thesis: ex t being transformation of F2,F1 st
for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (t . b) * (F2 /. f) = (F1 /. f) * (t . a)
take t1 " ; :: thesis: for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds ((t1 ") . b) * (F2 /. f) = (F1 /. f) * ((t1 ") . a)
thus for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds ((t1 ") . b) * (F2 /. f) = (F1 /. f) * ((t1 ") . a) by A1, A2, Lm4; :: thesis: verum