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

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

hence
q * (id B) = q
; :: thesis: verum(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;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