let B, C be non empty transitive with_units AltCatStr ; for G1, G2 being covariant Functor of B,C
for q being transformation of G1,G2 st G1 is_transformable_to G2 holds
q (#) (idt (id B)) = q
let G1, G2 be covariant Functor of B,C; for q being transformation of G1,G2 st G1 is_transformable_to G2 holds
q (#) (idt (id B)) = q
let q be transformation of G1,G2; ( G1 is_transformable_to G2 implies q (#) (idt (id B)) = q )
assume A1:
G1 is_transformable_to G2
; q (#) (idt (id B)) = q
then A2:
G1 * (id B) is_transformable_to G2 * (id B)
by Th10;
thus q (#) (idt (id B)) =
(q * (id B)) `*` (idt (G1 * (id B)))
by Th19
.=
q * (id B)
by A2, FUNCTOR2:5
.=
q
by A1, Th21
; verum