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
(idt (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
(idt (id B)) (#) p = p
let p be transformation of F1,F2; :: thesis: ( F1 is_transformable_to F2 implies (idt (id B)) (#) p = p )
assume A1: F1 is_transformable_to F2 ; :: thesis: (idt (id B)) (#) p = p
then A2: (id B) * F1 is_transformable_to (id B) * F2 by Th10;
thus (idt (id B)) (#) p = (idt ((id B) * F2)) `*` ((id B) * p) by Th18
.= (id B) * p by A2, FUNCTOR2:5
.= p by A1, Th20 ; :: thesis: verum