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

let i be set ; :: 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, FUNCTOR2:def 1;
thus ((id B) * p) . i = (id B) . (p ! a) by A1, Def1
.= p ! a by A2, FUNCTOR0:32
.= p . i by A1, FUNCTOR2:def 4 ; :: thesis: verum

end;

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