let A, B be Category; for F1, F2 being Functor of A,B
for s being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds
(id B) * s = s
let F1, F2 be Functor of A,B; for s being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds
(id B) * s = s
let s be natural_transformation of F1,F2; ( F1 is_naturally_transformable_to F2 implies (id B) * s = s )
assume A1:
F1 is_naturally_transformable_to F2
; (id B) * s = s
A2:
(id B) * F1 = F1
by FUNCT_2:17;
then reconsider t = (id B) * s as natural_transformation of F1,F2 by FUNCT_2:17;
A3:
(id B) * F2 = F2
by FUNCT_2:17;
hence
(id B) * s = s
by A1, Th24; verum