let S, T be NatTrans-DOMAIN of A,B; :: thesis: ( ( for x being set holds
( x in S iff ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st
( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ) ) ) & ( for x being set holds
( x in T iff ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st
( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ) ) ) implies S = T )
assume that
A4: for x being set holds
( x in S iff ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st
( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ) ) and
A5: for x being set holds
( x in T iff ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st
( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ) ) ; :: thesis: S = T

now

let x be set ; :: thesis: ( x in S iff x in T )
( x in S iff ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st
( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ) ) by A4;
hence ( x in S iff x in T ) by A5; :: thesis: verum

end;

hence S = T by TARSKI:2; :: thesis: verum