:: deftheorem Def2 defines DOMAIN-yielding ZF_REFLE:def 2 :
for W being Universe
for IT being Sequence of W holds
( IT is DOMAIN-yielding iff dom IT = On W );