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
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 T1 . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)] and
A3: 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
A4: 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 A2;
hence T1 . a = T2 . a by A3; :: thesis: verum
end;
export F1 is_naturally_transformable_to export F2 by A1, Th21;
then export F1 is_transformable_to export F2 ;
hence T1 = T2 by A4, NATTRA_1:19; :: thesis: verum