let B, C be non empty transitive with_units AltCatStr ; :: thesis: 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; :: thesis: 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; :: thesis: ( G1 is_transformable_to G2 implies q (#) (idt (id B)) = q )
assume A1: G1 is_transformable_to G2 ; :: thesis: 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 ; :: thesis: verum