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 * (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 * (id B) = q
let q be transformation of G1,G2; :: thesis: ( G1 is_transformable_to G2 implies q * (id B) = q )
assume A1: G1 is_transformable_to G2 ; :: thesis: q * (id B) = q

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

let i be object ; :: thesis: ( i in the carrier of B implies (q * (id B)) . i = q . i )
assume i in the carrier of B ; :: thesis: (q * (id B)) . i = q . i
then reconsider a = i as Object of B ;
thus (q * (id B)) . i = q ! ((id B) . a) by A1, Def2
.= q ! a by FUNCTOR0:29
.= q . i by A1, FUNCTOR2:def 4 ; :: thesis: verum

end;

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