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 )
then A2: F1 is_transformable_to F2 by Def7;
assume A3: t1 is invertible ; :: thesis: F2 is_naturally_transformable_to F1
hence F2 is_transformable_to F1 by A2, 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, A3, Lm4; :: thesis: verum