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
A7: 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
A8: 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 :: thesis: for x being object holds
( x in S iff x in T )
let x be object ; :: 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 A7;
hence ( x in S iff x in T ) by A8; :: thesis: verum
end;
hence S = T by TARSKI:2; :: thesis: verum