let A, B be Category; :: thesis: for F1, F2 being Functor of A,B st F1 is_transformable_to F2 holds
for t being transformation of F1,F2 st t is invertible holds
for a being Object of A holds F1 . a,F2 . a are_isomorphic
let F1, F2 be Functor of A,B; :: thesis: ( F1 is_transformable_to F2 implies for t being transformation of F1,F2 st t is invertible holds
for a being Object of A holds F1 . a,F2 . a are_isomorphic )
assume F1 is_transformable_to F2 ; :: thesis: for t being transformation of F1,F2 st t is invertible holds
for a being Object of A holds F1 . a,F2 . a are_isomorphic
let t be transformation of F1,F2; :: thesis: ( t is invertible implies for a being Object of A holds F1 . a,F2 . a are_isomorphic )
assume A1: t is invertible ; :: thesis: for a being Object of A holds F1 . a,F2 . a are_isomorphic
let a be Object of A; :: thesis: F1 . a,F2 . a are_isomorphic
take t . a ; :: according to CAT_1:def 20 :: thesis: t . a is invertible
thus t . a is invertible by A1; :: thesis: verum