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 holds
( (id F2) `*` t = t & t `*` (id F1) = t )
let F1, F2 be Functor of A,B; :: thesis: ( F1 is_transformable_to F2 implies for t being transformation of F1,F2 holds
( (id F2) `*` t = t & t `*` (id F1) = t ) )
assume A1: F1 is_transformable_to F2 ; :: thesis: for t being transformation of F1,F2 holds
( (id F2) `*` t = t & t `*` (id F1) = t )
let t be transformation of F1,F2; :: thesis: ( (id F2) `*` t = t & t `*` (id F1) = t )

now

let a be Object of A; :: thesis: ((id F2) `*` t) . a = t . a
A2: Hom (F1 . a),(F2 . a) <> {} by A1, Def2;
thus ((id F2) `*` t) . a = ((id F2) . a) * (t . a) by A1, Def6
.= (id (F2 . a)) * (t . a) by Th21
.= t . a by A2, CAT_1:57 ; :: thesis: verum

end;

hence (id F2) `*` t = t by A1, Th20; :: thesis: t `*` (id F1) = t

now

let a be Object of A; :: thesis: (t `*` (id F1)) . a = t . a
A3: Hom (F1 . a),(F2 . a) <> {} by A1, Def2;
thus (t `*` (id F1)) . a = (t . a) * ((id F1) . a) by A1, Def6
.= (t . a) * (id (F1 . a)) by Th21
.= t . a by A3, CAT_1:58 ; :: thesis: verum

end;

hence t `*` (id F1) = t by A1, Th20; :: thesis: verum