let A, B be Category; :: thesis: for F1, F2 being Functor of A,B st F1 is_naturally_transformable_to F2 holds
for t being natural_transformation of F1,F2 holds
( (id F2) `*` t = t & t `*` (id F1) = t )
let F1, F2 be Functor of A,B; :: thesis: ( F1 is_naturally_transformable_to F2 implies for t being natural_transformation of F1,F2 holds
( (id F2) `*` t = t & t `*` (id F1) = t ) )
assume A1: F1 is_naturally_transformable_to F2 ; :: thesis: for t being natural_transformation of F1,F2 holds
( (id F2) `*` t = t & t `*` (id F1) = t )
then A2: F1 is_transformable_to F2 by Def7;
let t be natural_transformation of F1,F2; :: thesis: ( (id F2) `*` t = t & t `*` (id F1) = t )
thus (id F2) `*` t = (id F2) `*` t by A1, Def9
.= t by A2, Th22 ; :: thesis: t `*` (id F1) = t
thus t `*` (id F1) = t `*` (id F1) by A1, Def9
.= t by A2, Th22 ; :: thesis: verum