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 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 B) * s = s
let s be natural_transformation of F1,F2; :: thesis: ( F1 is_naturally_transformable_to F2 implies (id B) * s = s )
assume A1: F1 is_naturally_transformable_to F2 ; :: thesis: (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;

now :: thesis: for a being Object of A holds t . a = s . a

let a be Object of A; :: thesis: t . a = s . a
A4: Hom ((F1 . a),(F2 . a)) <> {} by A1, Th23;
thus t . a = (id B) /. (s . a) by A1, A2, A3, Th21
.= (id B) . (s . a) by A4, CAT_3:def 10
.= s . a by FUNCT_1:18 ; :: thesis: verum

end;

hence (id B) * s = s by A1, Th24; :: thesis: verum