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

for G1 being covariant Functor of B,C

for H1 being covariant Functor of C,D

for p being transformation of F1,F2 st F1 is_transformable_to F2 holds

(H1 * G1) * p = H1 * (G1 * p)

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

for H1 being covariant Functor of C,D

for p being transformation of F1,F2 st F1 is_transformable_to F2 holds

(H1 * G1) * p = H1 * (G1 * p)

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

for p being transformation of F1,F2 st F1 is_transformable_to F2 holds

(H1 * G1) * p = H1 * (G1 * p)

let H1 be covariant Functor of C,D; :: thesis: for p being transformation of F1,F2 st F1 is_transformable_to F2 holds

(H1 * G1) * p = H1 * (G1 * p)

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

A1: (H1 * G1) * F2 = H1 * (G1 * F2) by FUNCTOR0:32;

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

assume A2: F1 is_transformable_to F2 ; :: thesis: (H1 * G1) * p = H1 * (G1 * p)

for G1 being covariant Functor of B,C

for H1 being covariant Functor of C,D

for p being transformation of F1,F2 st F1 is_transformable_to F2 holds

(H1 * G1) * p = H1 * (G1 * p)

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

for H1 being covariant Functor of C,D

for p being transformation of F1,F2 st F1 is_transformable_to F2 holds

(H1 * G1) * p = H1 * (G1 * p)

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

for p being transformation of F1,F2 st F1 is_transformable_to F2 holds

(H1 * G1) * p = H1 * (G1 * p)

let H1 be covariant Functor of C,D; :: thesis: for p being transformation of F1,F2 st F1 is_transformable_to F2 holds

(H1 * G1) * p = H1 * (G1 * p)

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

A1: (H1 * G1) * F2 = H1 * (G1 * F2) by FUNCTOR0:32;

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

assume A2: F1 is_transformable_to F2 ; :: thesis: (H1 * G1) * p = H1 * (G1 * p)

now :: thesis: for a being Object of A holds ((H1 * G1) * p) ! a = m ! a

hence
(H1 * G1) * p = H1 * (G1 * p)
by A2, Th10, FUNCTOR2:3; :: thesis: verumlet a be Object of A; :: thesis: ((H1 * G1) * p) ! a = m ! a

A3: ( (G1 * F1) . a = G1 . (F1 . a) & (G1 * F2) . a = G1 . (F2 . a) ) by FUNCTOR0:33;

A4: <^(F1 . a),(F2 . a)^> <> {} by A2;

thus ((H1 * G1) * p) ! a = (H1 * G1) . (p ! a) by A2, Th11

.= H1 . (G1 . (p ! a)) by A4, Th6

.= H1 . ((G1 * p) ! a) by A2, A3, Th11

.= (H1 * (G1 * p)) ! a by A2, Th10, Th11

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

end;A3: ( (G1 * F1) . a = G1 . (F1 . a) & (G1 * F2) . a = G1 . (F2 . a) ) by FUNCTOR0:33;

A4: <^(F1 . a),(F2 . a)^> <> {} by A2;

thus ((H1 * G1) * p) ! a = (H1 * G1) . (p ! a) by A2, Th11

.= H1 . (G1 . (p ! a)) by A4, Th6

.= H1 . ((G1 * p) ! a) by A2, A3, Th11

.= (H1 * (G1 * p)) ! a by A2, Th10, Th11

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