reconsider s = t as Function of [: the carrier of A, the carrier of B:], the carrier' of C ;
let T1, T2 be natural_transformation of export F1, export F2; :: thesis: ( ( 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 T1 . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)] ) & ( 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 T2 . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)] ) implies T1 = T2 )
assume that
A1: 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 T1 . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)] and
A2: 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 T2 . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)] ; :: thesis: T1 = T2

A3: now :: thesis: for a being Object of A holds T1 . a = T2 . a

let a be Object of A; :: thesis: T1 . a = T2 . a
T1 . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)] by A1;
hence T1 . a = T2 . a by A2; :: thesis: verum

end;

export F1 is_naturally_transformable_to export F2 by B1, Th23;
then export F1 is_transformable_to export F2 by NATTRA_1:def 7;
hence T1 = T2 by A3, NATTRA_1:19; :: thesis: verum