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 & (id B) * F2 = F2 ) by FUNCT_2:23;
then reconsider t = (id B) * s as natural_transformation of F1,F2 ;

now

let a be Object of A; :: thesis: t . a = s . a
A3: Hom (F1 . a),(F2 . a) <> {} by A1, Th30;
thus t . a = (id B) . (s . a) by A1, A2, Th28
.= (id B) . (s . a) by A3, NATTRA_1:def 1
.= s . a by FUNCT_1:35 ; :: thesis: verum

end;

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