let A, B, C, D be non empty transitive with_units AltCatStr ; :: thesis: for F1 being covariant Functor of A,B

for G1, G2 being covariant Functor of B,C

for H1 being covariant Functor of C,D

for q being transformation of G1,G2 st G1 is_transformable_to G2 holds

(H1 * q) * F1 = H1 * (q * F1)

let F1 be covariant Functor of A,B; :: thesis: for G1, G2 being covariant Functor of B,C

for H1 being covariant Functor of C,D

for q being transformation of G1,G2 st G1 is_transformable_to G2 holds

(H1 * q) * F1 = H1 * (q * F1)

let G1, G2 be covariant Functor of B,C; :: thesis: for H1 being covariant Functor of C,D

for q being transformation of G1,G2 st G1 is_transformable_to G2 holds

(H1 * q) * F1 = H1 * (q * F1)

let H1 be covariant Functor of C,D; :: thesis: for q being transformation of G1,G2 st G1 is_transformable_to G2 holds

(H1 * q) * F1 = H1 * (q * F1)

let q be transformation of G1,G2; :: thesis: ( G1 is_transformable_to G2 implies (H1 * q) * F1 = H1 * (q * F1) )

A1: (H1 * G2) * F1 = H1 * (G2 * F1) by FUNCTOR0:32;

then reconsider m = H1 * (q * F1) as transformation of (H1 * G1) * F1,(H1 * G2) * F1 by FUNCTOR0:32;

assume A2: G1 is_transformable_to G2 ; :: thesis: (H1 * q) * F1 = H1 * (q * F1)

hence (H1 * q) * F1 = H1 * (q * F1) by A3, Th10, FUNCTOR2:3; :: thesis: verum

for G1, G2 being covariant Functor of B,C

for H1 being covariant Functor of C,D

for q being transformation of G1,G2 st G1 is_transformable_to G2 holds

(H1 * q) * F1 = H1 * (q * F1)

let F1 be covariant Functor of A,B; :: thesis: for G1, G2 being covariant Functor of B,C

for H1 being covariant Functor of C,D

for q being transformation of G1,G2 st G1 is_transformable_to G2 holds

(H1 * q) * F1 = H1 * (q * F1)

let G1, G2 be covariant Functor of B,C; :: thesis: for H1 being covariant Functor of C,D

for q being transformation of G1,G2 st G1 is_transformable_to G2 holds

(H1 * q) * F1 = H1 * (q * F1)

let H1 be covariant Functor of C,D; :: thesis: for q being transformation of G1,G2 st G1 is_transformable_to G2 holds

(H1 * q) * F1 = H1 * (q * F1)

let q be transformation of G1,G2; :: thesis: ( G1 is_transformable_to G2 implies (H1 * q) * F1 = H1 * (q * F1) )

A1: (H1 * G2) * F1 = H1 * (G2 * F1) by FUNCTOR0:32;

then reconsider m = H1 * (q * F1) as transformation of (H1 * G1) * F1,(H1 * G2) * F1 by FUNCTOR0:32;

assume A2: G1 is_transformable_to G2 ; :: thesis: (H1 * q) * F1 = H1 * (q * F1)

A3: now :: thesis: for a being Object of A holds ((H1 * q) * F1) ! a = m ! a

H1 * G1 is_transformable_to H1 * G2
by A2, Th10;let a be Object of A; :: thesis: ((H1 * q) * F1) ! a = m ! a

A4: ( (G1 * F1) . a = G1 . (F1 . a) & (G2 * F1) . a = G2 . (F1 . a) ) by FUNCTOR0:33;

thus ((H1 * q) * F1) ! a = (H1 * q) ! (F1 . a) by A2, Th10, Th12

.= H1 . (q ! (F1 . a)) by A2, Th11

.= H1 . ((q * F1) ! a) by A2, A4, Th12

.= (H1 * (q * F1)) ! a by A2, Th10, Th11

.= m ! a by A1, FUNCTOR0:32 ; :: thesis: verum

end;A4: ( (G1 * F1) . a = G1 . (F1 . a) & (G2 * F1) . a = G2 . (F1 . a) ) by FUNCTOR0:33;

thus ((H1 * q) * F1) ! a = (H1 * q) ! (F1 . a) by A2, Th10, Th12

.= H1 . (q ! (F1 . a)) by A2, Th11

.= H1 . ((q * F1) ! a) by A2, A4, Th12

.= (H1 * (q * F1)) ! a by A2, Th10, Th11

.= m ! a by A1, FUNCTOR0:32 ; :: thesis: verum

hence (H1 * q) * F1 = H1 * (q * F1) by A3, Th10, FUNCTOR2:3; :: thesis: verum