let A, B be Category; :: thesis: 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 (id B)) (#) s = s
let F1, F2 be Functor of A,B; :: thesis: for s being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds
(id (id B)) (#) s = s
let s be natural_transformation of F1,F2; :: thesis: ( F1 is_naturally_transformable_to F2 implies (id (id B)) (#) s = s )
assume A1: F1 is_naturally_transformable_to F2 ; :: thesis: (id (id B)) (#) s = s
then A2: (id B) * F1 is_naturally_transformable_to (id B) * F2 by Th20;
thus (id (id B)) (#) s = (id ((id B) * F2)) `*` ((id B) * s) by Th30
.= (id B) * s by A2, NATTRA_1:24
.= s by A1, Th33 ; :: thesis: verum