theorem Th35:
for
A,
B,
C being
Category for
F1,
G1 being
Functor of
A,
B for
F2,
G2 being
Functor of
A,
C st
F1 is_transformable_to G1 &
F2 is_transformable_to G2 holds
for
t1 being
transformation of
F1,
G1 for
t2 being
transformation of
F2,
G2 for
a being
Object of
A holds
<:t1,t2:> . a = [(t1 . a),(t2 . a)]