theorem Th21:
for
A,
B,
C being
Category for
F1,
F2 being
Functor of
[:A,B:],
C st
F1 is_naturally_transformable_to F2 holds
for
t being
natural_transformation of
F1,
F2 holds
(
export F1 is_naturally_transformable_to export F2 & ex
G being
natural_transformation of
export F1,
export F2 st
for
s being
Function of
[: the carrier of A, the carrier of B:], the
carrier' of
C st
t = s holds
for
a being
Object of
A holds
G . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)] )