let A, B be non empty transitive with_units AltCatStr ; :: thesis: for F1, F2 being covariant Functor of A,B
for p being transformation of F1,F2 st F1 is_transformable_to F2 holds
(id B) * p = p
let F1, F2 be covariant Functor of A,B; :: thesis: for p being transformation of F1,F2 st F1 is_transformable_to F2 holds
(id B) * p = p
let p be transformation of F1,F2; :: thesis: ( F1 is_transformable_to F2 implies (id B) * p = p )
assume A1: F1 is_transformable_to F2 ; :: thesis: (id B) * p = p

now :: thesis: for i being object st i in the carrier of A holds
((id B) * p) . i = p . i

let i be object ; :: thesis: ( i in the carrier of A implies ((id B) * p) . i = p . i )
assume i in the carrier of A ; :: thesis: ((id B) * p) . i = p . i
then reconsider a = i as Object of A ;
A2: <^(F1 . a),(F2 . a)^> <> {} by A1;
thus ((id B) * p) . i = (id B) . (p ! a) by A1, Def1
.= p ! a by A2, FUNCTOR0:31
.= p . i by A1, FUNCTOR2:def 4 ; :: thesis: verum

end;

hence (id B) * p = p ; :: thesis: verum